pub proof fn vm_reader_skip_embedded(tracked owner: &mut VmIoOwner, nbytes: usize)Expand description
requires
old(owner).inv(),ensuresfinal(owner).inv(),*final(owner) == *old(owner),Mirror of crate::mm::io::VmReader::skip.
Exec only mutates the handle’s cursor field (no owner mutation).