pub proof fn vm_reader_limit_embedded(tracked owner: &mut VmIoOwner, max_remain: usize)Expand description
requires
old(owner).inv(),final(owner).inv(),*final(owner) == *old(owner),Mirror of crate::mm::io::VmReader::limit.
Exec only mutates the handle’s end field (no owner mutation), so
owner state is fully preserved.