Struct TLVal 

pub struct TLVal<Tag, Len, Body>(pub Body, pub PhantomData<(Tag, Len)>);

One of the dependent family of combinators

Typically used as Implicit((U8, U16Le), TLVOf(body)).

Tuple Fields

0: Body

1: PhantomData<(Tag, Len)>

Trait Implementations

impl<Tag, Len, V> DepCombinator for TLVal<Tag, Len, V>

where Len: AsLen, V: DepCombinator<Key = Tag>, V::Body: SpecByteLen<T = V::Val>,

open spec fn apply(&self, key: Self::Key) -> Self::Body

{
    let (tag, len) = key;
    ExactLen(len, self.0.apply(tag))
}

open spec fn recover(&self, value: Self::Val) -> Self::Key

{
    let tag = self.0.recover(value);
    let body = self.0.apply(tag);
    (tag, Len::as_self(body.byte_len(value)))
}

open spec fn recover_inv(&self) -> bool

{ self.0.recover_inv() }

proof fn lemma_recover_consistent(&self, key: Self::Key, value: Self::Val)

type Key = (Tag, Len)

The type of keys parsed by the head combinator/to be recovered during serialization.

type Val = <V as DepCombinator>::Val

The type of values consumed/produced by the body combinator.

type Body = ExactLen<<V as DepCombinator>::Body, Len>

The type of the body combinator produced by apply.