Struct OutputSlice 

pub struct OutputSlice<'a> {
    pub obuf: &'a mut [u8],
    pub pos: usize,
}

A non-allocating append sink backed by a caller-provided slice.

Its logical view is the prefix written so far (given by pos).

Fields

obuf: &'a mut [u8]

pos: usize

Implementations

impl<'a> OutputSlice<'a>

pub open spec fn final_destination(&self) -> Seq<u8>

{ final(self.obuf)@ }

The prophetic final contents of the caller-provided backing slice.

pub exec fn new(obuf: &'a mut [u8]) -> output : Self

ensures

output@ == Seq::empty(),

output.fits(old(obuf)@.len()),

forall |len: nat| #[trigger] output.fits(len) == (len <= old(obuf)@.len()),

output.final_destination() == final(obuf)@,

Creates an empty logical output over obuf without allocating.

Trait Implementations

impl OutputBuf for OutputSlice<'_>

open spec fn fits(&self, len: nat) -> bool

{ self.pos as nat + len <= self.obuf@.len() }

proof fn lemma_fits_mono(&self, shorter: nat, longer: nat)

open spec fn same_destination(&self, other: &Self) -> bool

{ self.final_destination() == other.final_destination() }

proof fn lemma_same_destination_reflexive(&self)

proof fn lemma_same_destination_transitive(&self, _middle: &Self, _last: &Self)

exec fn write_byte(&mut self, byte: u8)

exec fn write_bytes(&mut self, bytes: &[u8])

impl View for OutputSlice<'_>

open spec fn view(&self) -> Self::V

{ self.obuf@.take(self.pos as int) }

type V = Seq<u8>