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

Function vm_writer_fill_zeros_embedded

pub proof fn vm_writer_fill_zeros_embedded(tracked owner: &mut VmIoOwner, len: usize)

Expand description

requires

old(owner).inv(),

ensures

final(owner).inv(),

final(owner).mem_view == old(owner).mem_view,

final(owner).range == old(owner).range,

Mirror of crate::mm::io::VmWriter::fill_zeros.

Exec body writes through self.cursor and then advances the handle’s cursor; the owner’s mem_view shape is preserved (write view stays a write view).

vm_writer_fill_zeros_embedded

Function vm_writer_fill_zeros_embedded Copy item path

Function vm_writer_fill_zeros_embedded