pub proof fn vm_writer_limit_embedded(tracked owner: &mut VmIoOwner, max_avail: usize)Expand description
requires
old(owner).inv(),final(owner).inv(),*final(owner) == *old(owner),Mirror of crate::mm::io::VmWriter::limit.