Trait VestOutput

Source

pub trait VestOutput<I>: View<V = Seq<u8>>where
    I: View<V = Seq<u8>>,{
    // Required methods
    exec fn len(&self) -> res : usize;
    exec fn set_range(&mut self, i: usize, input: &I);
}

Expand description

Trait for types that can be used as output for Vest serializers. VestOutput does not expose the contents of the buffer, so opaque buffer types for side-channel security can implement VestOutput.

Required Methods§

Source

exec fn len(&self) -> res : usize

ensures

res == self@.len(),

The length of the buffer.

Source

exec fn set_range(&mut self, i: usize, input: &I)

requires

0 <= i + input@.len() <= old(self)@.len() <= usize::MAX,

ensures

self@.len() == old(self)@.len()
    && self@
        == old(self)@
            .subrange(0, i as int)
            .add(input@)
            .add(old(self)@.subrange(i + input@.len(), self@.len() as int)),

Copy input to self starting at index i.