Trait OutputBuf 

pub trait OutputBuf: View<V = Seq<u8>> {
    // Required methods
    spec fn fits(&self, len: nat) -> bool;
    broadcast proof fn lemma_fits_mono(&self, shorter: nat, longer: nat);
    spec fn same_destination(&self, other: &Self) -> bool;
    broadcast proof fn lemma_same_destination_reflexive(&self);
    broadcast proof fn lemma_same_destination_transitive(&self, middle: &Self, last: &Self);
    exec fn write_byte(&mut self, byte: u8);

    // Provided method
    exec fn write_bytes(&mut self, bytes: &[u8]) { ... }
}

An abstraction for append-oriented output buffer.

The view is the sequence already present in, or written through, the output. Capacity is abstract: bounded and unbounded outputs expose the same fits interface.

Required Methods

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

Whether the output can accept len additional bytes.

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

requires

shorter <= longer,

self.fits(longer),

ensures

self.fits(shorter),

Write capacity is monotone: accepting a larger write implies accepting every prefix.

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

Whether two states write to the same final destination.

This is vacuously true for outputs without (re-)borrowed backing storage. For a borrowed output, it relates the prophetic final contents of the backing storage across states.

broadcast proof fn lemma_same_destination_reflexive(&self)

ensures

#[trigger] self.same_destination(self),

Destination identity is reflexive.

broadcast proof fn lemma_same_destination_transitive(&self, middle: &Self, last: &Self)

requires

self.same_destination(middle),

middle.same_destination(last),

ensures

self.same_destination(last),

Destination identity is transitive.

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

requires

old(self).fits(1),

ensures

final(self)@ == old(self)@.push(byte),

forall |n| old(self).fits(1 + n) <==> #[trigger] final(self).fits(n),

old(self).same_destination(final(self)),

Appends one byte to the logical output.

Provided Methods

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

requires

old(self).fits(bytes@.len()),

ensures

final(self)@ == old(self)@ + bytes@,

forall |n| old(self).fits(bytes@.len() + n) <==> #[trigger] final(self).fits(n),

old(self).same_destination(final(self)),

Appends all bytes in bytes to the logical output.

Dyn Compatibility

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementations on Foreign Types

impl OutputBuf for Vec<u8>

Available on crate feature alloc only.

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

{ true }

proof fn lemma_fits_mono(&self, _shorter: nat, _longer: nat)

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

{ true }

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])

Implementors

impl OutputBuf for OutputSlice<'_>