Trait VestPublicOutput

Source

pub trait VestPublicOutput<I>: VestOutput<I>where
    I: View<V = Seq<u8>>,{
    // Required methods
    exec fn set_byte(&mut self, i: usize, value: u8);
    exec fn set_byte_range(&mut self, i: usize, input: &[u8]);
}

Expand description

Trait for types that can be used as output for Vest serializers. VestPublicOutput can be set using transparent bytes, so it cannot provide type abstraction for side-channel security.

Required Methods§

Source

exec fn set_byte(&mut self, i: usize, value: u8)

requires

i < old(self)@.len(),

ensures

self@ == old(self)@.update(i as int, value),

Set the byte at index i to value.

Source

exec fn set_byte_range(&mut self, i: usize, input: &[u8])

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. (Same as set_range but with byte slice input.)