Struct Varied 

pub struct Varied<Len = u8>(pub Len);

Parses/serializes a variable-length byte sequence Seq<u8>.

The length is determined by self.0, which must implement super::length::AsLen and defaults to u8.

Consistency

A byte sequence is consistent w.r.t Varied iff its length equals self.0.

Tuple Fields

0: Len

Implementations

impl<Len: AsLen> Varied<Len>

pub open spec fn byte_len(v: <Self as SpecByteLen>::T) -> nat

{ v.len() }

Trait Implementations

impl<'i, Len: AsLen> ByteLen<&'i [u8]> for Varied<Len>

exec fn length(&self, v: &&'i [u8]) -> len : usize

fn exec_inv(&self) -> bool

impl<Len: AsLen> ByteLen<[u8]> for Varied<Len>

exec fn length(&self, v: &[u8]) -> len : usize

fn exec_inv(&self) -> bool

impl<Len: AsLen> BytesCombinator for Varied<Len>

proof fn lemma_byte_len_is_buf_len(&self, s: Seq<u8>)

impl<Len: Clone> Clone for Varied<Len>

exec fn clone(&self) -> cloned : Self

ensures

call_ensures(Len::clone, (&self.0,), cloned.0),

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl<Len: AsLen> Consistency for Varied<Len>

open spec fn consistent(&self, v: Self::Val) -> bool

{ v.len() == self.0.as_nat() }

type Val = Seq<u8>

The type of values whose consistency is being checked.

impl<Len: AsLen> EquivSerializers for Varied<Len>

proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SVal)

fn equiv_inv(&self) -> bool

impl<Len: AsLen> EquivSerializersGeneral for Varied<Len>

proof fn lemma_serialize_equiv(&self, v: Self::SVal, obuf: Seq<u8>)

fn equiv_general_inv(&self) -> bool

impl<Len: AsLen> GoodSerializer for Varied<Len>

proof fn lemma_serialize_len(&self, v: Self::SVal)

fn serialize_inv(&self) -> bool

impl<Len: AsLen> LeafNonMalleable for Varied<Len>

proof fn nonmal_leaf_inv(&self)

impl<Len: AsLen> MinMaxByteLen for Varied<Len>

open spec fn min(&self) -> nat

{ self.0.as_nat() }

open spec fn max(&self) -> nat

{ self.0.as_nat() }

proof fn lemma_min_max_byte_len(&self, v: Self::T)

impl<Len: AsLen> NoLookAhead for Varied<Len>

proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>)

fn no_lookahead_inv(&self) -> bool

fn corollary_non_extensible(&self, i1: Seq<u8>, i2: Seq<u8>)

impl<Len: AsLen> NonMalleable for Varied<Len>

proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>)

fn nonmal_inv(&self) -> bool

impl<Len: AsLen> NonTailFmt for Varied<Len>

proof fn lemma_serialize_dps_prepend(&self, v: Seq<u8>, obuf: Seq<u8>)

proof fn lemma_serialize_dps_len(&self, v: Seq<u8>, obuf: Seq<u8>)

fn serialize_dps_inv(&self) -> bool

impl<Len: AsLen, I: InputBuf> Parser<I> for Varied<Len>

exec fn parse(&self, ibuf: &I) -> PResult<Self::PT>

type PT = I

Executable value returned by this parser.

fn exec_inv(&self) -> bool

impl<'i, Len: AsLen> Prepare<&'i [u8]> for Varied<Len>

exec fn prepare(&self, v: &&'i [u8]) -> checked : Result<usize, PreSerializeError>

fn exec_inv(&self) -> bool

impl<Len: AsLen> Prepare<[u8]> for Varied<Len>

exec fn prepare(&self, v: &[u8]) -> checked : Result<usize, PreSerializeError>

fn exec_inv(&self) -> bool

impl<Len: AsLen> Productive for Varied<Len>

open spec fn productive_inv(&self) -> bool

{ self.0.as_nat() > 0 }

proof fn lemma_productive(&self, s: Seq<u8>)

impl<Len: AsLen> SPRoundTripDps for Varied<Len>

proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::T, obuf: Seq<u8>)

fn unambiguous(&self) -> bool

impl<Len: AsLen> SafeParser for Varied<Len>

proof fn lemma_parse_safe(&self, ibuf: Seq<u8>)

fn safe_inv(&self) -> bool

impl<'i, Output: OutputBuf, Len: AsLen> Serializer<Output, &'i [u8]> for Varied<Len>

exec fn serialize_into(&self, v: &&'i [u8], obuf: &mut Output)

fn exec_inv(&self) -> bool

impl<Output: OutputBuf, Len: AsLen> Serializer<Output, [u8]> for Varied<Len>

exec fn serialize_into(&self, v: &[u8], obuf: &mut Output)

fn exec_inv(&self) -> bool

impl<Len: AsLen> SoundParser for Varied<Len>

proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>)

proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>)

fn sound_inv(&self) -> bool

impl<Len: AsLen> SpecByteLen for Varied<Len>

open spec fn byte_len(&self, v: Self::T) -> nat

{ v.len() }

type T = Seq<u8>

The type of values whose byte length is being computed.

impl<Len: AsLen> SpecParser for Varied<Len>

open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)>

{
    if ibuf.len() < self.0.as_nat() {
        None
    } else {
        Some((self.0.as_nat() as int, ibuf.take(self.0.as_nat() as int)))
    }
}

type PVal = Seq<u8>

The type of parsed values.

impl<Len: AsLen> SpecSerializer for Varied<Len>

open spec fn spec_serialize(&self, v: Self::SVal) -> Seq<u8>

{ v }

type SVal = Seq<u8>

The type of values to be serialized.

impl<Len: AsLen> SpecSerializerDps for Varied<Len>

open spec fn spec_serialize_dps(&self, v: Self::SValue, obuf: Seq<u8>) -> Seq<u8>

{ v + obuf }

type SValue = Seq<u8>

The type of values to be serialized.

impl<Len: AsLen> ValueByteLen for Varied<Len>

open spec fn value_byte_len(v: Self::T) -> nat

{ v.len() }

proof fn lemma_value_len_matches_byte_len(&self, v: Self::T)

impl<Len: Copy> Copy for Varied<Len>