Skip to main content

vm_writer_write_embedded

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

Function vm_writer_write_embedded 

Source 
pub proof fn vm_writer_write_embedded(tracked 
    source_owner: &mut VmIoOwner,
tracked     dest_owner: &mut VmIoOwner,
)
Expand description
requires
old(source_owner).inv(),
old(dest_owner).inv(),
old(source_owner).read_view_initialized(),
old(dest_owner).has_write_view(),
ensures
final(source_owner).inv(),
final(dest_owner).inv(),
final(source_owner).read_view_initialized(),
final(dest_owner).has_write_view(),
final(source_owner).range.start >= old(source_owner).range.start,
final(source_owner).range.end == old(source_owner).range.end,
final(dest_owner).range.start >= old(dest_owner).range.start,
final(dest_owner).range.end == old(dest_owner).range.end,

Mirror of crate::mm::io::VmWriter::write (Infallible).

Exec no longer surfaces consumed_w (the body delegates to reader.read(self) and discards its split-off output). So this axiom mutates both owners but produces nothing new.