Skip to main content

vm_reader_read_embedded

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

Function vm_reader_read_embedded 

Source 
pub proof fn vm_reader_read_embedded(tracked 
    source_owner: &mut VmIoOwner,
tracked     dest_owner: &mut VmIoOwner,
) -> tracked consumed_w : 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,
consumed_w.inv(),
consumed_w.has_write_view(),
consumed_w.range.start >= old(dest_owner).range.start,
consumed_w.range.end <= final(dest_owner).range.start,

Mirror of crate::mm::io::VmReader::read (Infallible).

Exec requires: self.inv(), writer.inv(), self.wf(owner_r), writer.wf(owner_w), owner_w.has_write_view(), owner_r.read_view_initialized().

Expressible: owner inv, has_write_view, read_view_initialized. MODEL GAP: handle inv/wf.