VestInput

vest_lib::buf_traits

Trait VestInput 

Source 
pub trait VestInput: View<V = Seq<u8>> {
    // Required methods
    exec fn len(&self) -> res : usize;
    exec fn subrange(&self, i: usize, j: usize) -> res : Self
       where Self: Sized;
    exec fn clone(&self) -> res : Self
       where Self: Sized;
}
Expand description

Trait definitions Trait for types that can be used as input for Vest parsers, roughly corresponding to byte buffers. VestInput does not expose the contents of the buffer, so opaque buffer types for side-channel security can implement VestInput.

Required Methods§

Source

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

ensures
res == self@.len(),

The length of the buffer.

Source

exec fn subrange(&self, i: usize, j: usize) -> res : Self
where Self: Sized,

requires
0 <= i <= j <= self@.len(),
ensures
res@ == self@.subrange(i as int, j as int),

Analogous to vstd::slice_subrange

Source

exec fn clone(&self) -> res : Self
where Self: Sized,

ensures
res@ == self@,

Creates another buffer with the same contents. For good performance, this function should be cheap, just creating a new reference rather than actually copying the buffer.

Implementations on Foreign Types§

Source§

impl<'a> VestInput for &'a [u8]

Implementations for common types

Source§

exec fn len(&self) -> usize

Source§

exec fn subrange(&self, i: usize, j: usize) -> &'a [u8] ⓘ

Source§

exec fn clone(&self) -> &'a [u8] ⓘ

Implementors§