Type Alias BundledSpecs 

pub type BundledSpecs<T> = (PredFnSpec<T>, ByteLenFnSpec<T>, ParserFnSpec<T>, SerializerFnSpec<T>, SerializerDPSFnSpec<T>);

Trait Implementations

impl<T> Consistency for BundledSpecs<T>

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

{ (self.0)(v) }

type Val = T

The type of values whose consistency is being checked.

impl<T> EquivSerializers for BundledSpecs<T>

open spec fn equiv_inv(&self) -> bool

{
    let (_, _, _, s, s_dps) = *self;
    forall |v: T| #[trigger] (s_dps)(v, seq![]) == (s)(v) + seq![]
}

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

impl<T> EquivSerializersGeneral for BundledSpecs<T>

open spec fn equiv_general_inv(&self) -> bool

{
    let (_, _, _, s, s_dps) = *self;
    forall |v: T, obuf: Seq<u8>| #[trigger] (s_dps)(v, obuf) == (s)(v) + obuf
}

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

impl<T> GoodSerializer for BundledSpecs<T>

open spec fn serialize_inv(&self) -> bool

{ serializer_specs(*self).serialize_inv() }

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

impl<T> NoLookAhead for BundledSpecs<T>

open spec fn no_lookahead_inv(&self) -> bool

{
    let (_, _, p, _, _) = *self;
    no_lookahead_parser(p)
}

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

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

impl<T> NonMalleable for BundledSpecs<T>

open spec fn nonmal_inv(&self) -> bool

{ parser_specs(*self).nonmal_inv() }

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

impl<T> NonTailFmt for BundledSpecs<T>

open spec fn serialize_dps_inv(&self) -> bool

{
    let (_, b, _, _, s_dps) = *self;
    non_tail_fmt_dps(s_dps, b)
}

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

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

impl<T> Productive for BundledSpecs<T>

open spec fn productive_inv(&self) -> bool

{ parser_specs(*self).productive_inv() }

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

impl<T> SPRoundTripDps for BundledSpecs<T>

open spec fn unambiguous(&self) -> bool

{
    let (c, b, p, _, s_dps) = *self;
    sp_roundtrip_dps(p, c, b, s_dps)
}

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

impl<T> SafeParser for BundledSpecs<T>

open spec fn safe_inv(&self) -> bool

{ parser_specs(*self).safe_inv() }

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

impl<T> SoundParser for BundledSpecs<T>

open spec fn sound_inv(&self) -> bool

{ parser_specs(*self).sound_inv() }

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

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

impl<T> SpecByteLen for BundledSpecs<T>

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

{ (self.1)(v) }

type T = T

The type of values whose byte length is being computed.

impl<T> SpecParser for BundledSpecs<T>

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

{ (self.2)(input) }

type PVal = T

The type of parsed values.

impl<T> SpecSerializer for BundledSpecs<T>

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

{ (self.3)(v) }

type SVal = T

The type of values to be serialized.

impl<T> SpecSerializerDps for BundledSpecs<T>

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

{ (self.4)(v, obuf) }

type SValue = T

The type of values to be serialized.