Type Alias SerializerSpecs 

pub type SerializerSpecs<SpecS, Blen> = (SpecS, Blen);

A bundled non-DPS serializer: pairs a SerializerFnSpec with a ByteLenFnSpec.

Trait Implementations

impl<SpecS, Blen> GoodSerializer for SerializerSpecs<SpecS, Blen>

where Blen: SpecByteLen, SpecS: SpecSerializer<SVal = Blen::T>,

open spec fn serialize_inv(&self) -> bool

{
    let (s, b) = *self;
    let (s_fn, b_fn) = (|v| s.spec_serialize(v), |v| b.byte_len(v));
    good_serializer_fn(s_fn, b_fn)
}

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

impl<SpecS, Blen> SpecByteLen for SerializerSpecs<SpecS, Blen>

where Blen: SpecByteLen, SpecS: SpecSerializer<SVal = Blen::T>,

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

{ (self.1).byte_len(v) }

type T = <Blen as SpecByteLen>::T

The type of values whose byte length is being computed.

impl<SpecS, Blen> SpecSerializer for SerializerSpecs<SpecS, Blen>

where Blen: SpecByteLen, SpecS: SpecSerializer<SVal = Blen::T>,

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

{ (self.0).spec_serialize(v) }

type SVal = <Blen as SpecByteLen>::T

The type of values to be serialized.