Struct PrefixTagged 

pub struct PrefixTagged<Tg, Tag, Of>(pub Tg, pub Tag, pub Of);

Sugar for Preceded { a: Const(inner, tag), a_val: tag, b: body }.

Tuple Fields

0: Tg

1: Tag

2: Of

Trait Implementations

impl<Tg, TagVal, Of, T> ByteLen<T> for PrefixTagged<Tg, TagVal, Of>

where Tg: SpecByteLen<T = TagVal> + ByteLen<TagVal>, TagVal: DeepView<V = TagVal> + PartialEq + Structural + Copy, T: DeepView, Of: ByteLen<T>,

open spec fn exec_inv(&self) -> bool

{
    &&& self.0.exec_inv()
    &&& self.2.exec_inv()
    &&& forall |v: TagVal| v.deep_view() == v

}

exec fn length(&self, v: &T) -> len : usize

impl<Tg: Clone, Tag: Clone, Of: Clone> Clone for PrefixTagged<Tg, Tag, Of>

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

ensures

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

call_ensures(Tag::clone, (&self.1,), cloned.1),

call_ensures(Of::clone, (&self.2,), cloned.2),

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

Performs copy-assignment from source.

impl<Tg, Of> Consistency for PrefixTagged<Tg, Tg::T, Of>

where Tg: SpecByteLen + Consistency<Val = Tg::T>, Of: Consistency,

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

{ with_prefix_tag(self.0, self.1, self.2).consistent(v) }

type Val = <Of as Consistency>::Val

The type of values whose consistency is being checked.

impl<Tg, Of> EquivSerializers for PrefixTagged<Tg, Tg::T, Of>

where Tg: SpecByteLen + EquivSerializersGeneral<SVal = Tg::T, SValue = Tg::T> + Consistency<Val = Tg::T>, Of: EquivSerializers,

open spec fn equiv_inv(&self) -> bool

{ with_prefix_tag(self.0, self.1, self.2).equiv_inv() }

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

impl<Tg, Of> EquivSerializersGeneral for PrefixTagged<Tg, Tg::T, Of>

where Tg: SpecByteLen + EquivSerializersGeneral<SVal = Tg::T, SValue = Tg::T> + Consistency<Val = Tg::T>, Of: EquivSerializersGeneral,

open spec fn equiv_general_inv(&self) -> bool

{ with_prefix_tag(self.0, self.1, self.2).equiv_general_inv() }

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

impl<Tg, Of> GoodSerializer for PrefixTagged<Tg, Tg::T, Of>

where Tg: SpecByteLen + GoodSerializer, Of: GoodSerializer,

open spec fn serialize_inv(&self) -> bool

{ with_prefix_tag(self.0, self.1, self.2).serialize_inv() }

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

impl<Tg, Of> MinMaxByteLen for PrefixTagged<Tg, Tg::T, Of>

where Tg: SpecByteLen + MinMaxByteLen, Of: MinMaxByteLen,

open spec fn min(&self) -> nat

{ with_prefix_tag(self.0, self.1, self.2).min() }

open spec fn max(&self) -> nat

{ with_prefix_tag(self.0, self.1, self.2).max() }

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

impl<Tg, Of> NoLookAhead for PrefixTagged<Tg, Tg::T, Of>

where Tg: SpecByteLen + NoLookAhead<PVal = Tg::T>, Of: NoLookAhead,

open spec fn no_lookahead_inv(&self) -> bool

{ with_prefix_tag(self.0, self.1, self.2).no_lookahead_inv() }

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

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

impl<Tg, Of> NonMalleable for PrefixTagged<Tg, Tg::T, Of>

where Tg: SpecByteLen + SoundParser + NonMalleable, Of: SoundParser + NonMalleable,

open spec fn nonmal_inv(&self) -> bool

{ with_prefix_tag(self.0, self.1, self.2).nonmal_inv() }

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

impl<Tg, Of> NonTailFmt for PrefixTagged<Tg, Tg::T, Of>

where Tg: SpecByteLen + NonTailFmt, Of: NonTailFmt,

open spec fn serialize_dps_inv(&self) -> bool

{ with_prefix_tag(self.0, self.1, self.2).serialize_dps_inv() }

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<I, Tg, TagVal, Of> Parser<I> for PrefixTagged<Tg, TagVal, Of>

where I: InputBuf, Tg: SpecByteLen<T = TagVal> + Parser<I, PT = TagVal, PVal = TagVal> + SafeParser, TagVal: DeepView<V = TagVal> + PartialEq + Structural + Copy, Of: Parser<I> + SafeParser,

open spec fn exec_inv(&self) -> bool

{
    Preceded::<_, _, _, false> {
        a: super::Const(&self.0, self.1),
        b: &self.2,
        a_val: self.1,
    }
        .exec_inv()
}

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

type PT = <Of as Parser<I>>::PT

Executable value returned by this parser.

impl<Tg, TagVal, Of, T> Prepare<T> for PrefixTagged<Tg, TagVal, Of>

where Tg: SpecByteLen<T = TagVal> + Prepare<TagVal>, TagVal: DeepView<V = TagVal> + PartialEq + Structural + Copy, T: DeepView, Of: Prepare<T>,

open spec fn exec_inv(&self) -> bool

{
    &&& self.0.exec_inv()
    &&& self.2.exec_inv()
    &&& forall |v: TagVal| v.deep_view() == v

}

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

impl<Tg, Of> Productive for PrefixTagged<Tg, Tg::T, Of>

where Tg: SpecByteLen + Productive<PVal = Tg::T>, Of: Productive,

open spec fn productive_inv(&self) -> bool

{ with_prefix_tag(self.0, self.1, self.2).productive_inv() }

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

impl<Tg, Of> SPRoundTripDps for PrefixTagged<Tg, Tg::T, Of>

where Tg: SpecByteLen + SPRoundTripDps + NonTailFmt, Of: SPRoundTripDps,

open spec fn unambiguous(&self) -> bool

{ with_prefix_tag(self.0, self.1, self.2).unambiguous() }

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

impl<Tg, Of> SafeParser for PrefixTagged<Tg, Tg::T, Of>

where Tg: SpecByteLen + SafeParser<PVal = Tg::T>, Of: SafeParser,

open spec fn safe_inv(&self) -> bool

{ with_prefix_tag(self.0, self.1, self.2).safe_inv() }

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

impl<Output: OutputBuf, Tg, TagVal, Of, T> Serializer<Output, T> for PrefixTagged<Tg, TagVal, Of>

where Tg: SpecByteLen<T = TagVal> + Serializer<Output, TagVal>, TagVal: DeepView<V = TagVal> + PartialEq + Structural + Copy, T: DeepView, Of: Serializer<Output, T>,

open spec fn exec_inv(&self) -> bool

{
    &&& self.0.exec_inv()
    &&& self.2.exec_inv()
    &&& forall |v: Tg::T| v.deep_view() == v

}

exec fn serialize_into(&self, v: &T, obuf: &mut Output)

impl<Tg, Of> SoundParser for PrefixTagged<Tg, Tg::T, Of>

where Tg: SpecByteLen + SoundParser, Of: SoundParser,

open spec fn sound_inv(&self) -> bool

{ with_prefix_tag(self.0, self.1, self.2).sound_inv() }

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

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

impl<Tg, Of> SpecByteLen for PrefixTagged<Tg, Tg::T, Of>

where Tg: SpecByteLen, Of: SpecByteLen,

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

{ with_prefix_tag(self.0, self.1, self.2).byte_len(v) }

type T = <Of as SpecByteLen>::T

The type of values whose byte length is being computed.

impl<Tg, Of> SpecParser for PrefixTagged<Tg, Tg::T, Of>

where Tg: SpecByteLen + SpecParser<PVal = Tg::T>, Of: SpecParser,

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

{ with_prefix_tag(self.0, self.1, self.2).spec_parse(ibuf) }

type PVal = <Of as SpecParser>::PVal

The type of parsed values.

impl<Tg, Of> SpecSerializer for PrefixTagged<Tg, Tg::T, Of>

where Tg: SpecByteLen + SpecSerializer<SVal = Tg::T>, Of: SpecSerializer,

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

{ with_prefix_tag(self.0, self.1, self.2).spec_serialize(v) }

type SVal = <Of as SpecSerializer>::SVal

The type of values to be serialized.

impl<Tg, Of> SpecSerializerDps for PrefixTagged<Tg, Tg::T, Of>

where Tg: SpecByteLen + SpecSerializerDps<SValue = Tg::T>, Of: SpecSerializerDps,

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

{ with_prefix_tag(self.0, self.1, self.2).spec_serialize_dps(v, obuf) }

type SValue = <Of as SpecSerializerDps>::SValue

The type of values to be serialized.

impl<Tg, Of> StaticByteLen for PrefixTagged<Tg, Tg::T, Of>

where Tg: StaticByteLen, Of: StaticByteLen,

open spec fn static_byte_len() -> nat

{ Tg::static_byte_len() + Of::static_byte_len() }

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

impl<Tg, Of> ValueByteLen for PrefixTagged<Tg, Tg::T, Of>

where Tg: StaticByteLen, Of: ValueByteLen,

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

{ Tg::static_byte_len() + Of::value_byte_len(v) }

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

impl<Tg: Copy, Tag: Copy, Of: Copy> Copy for PrefixTagged<Tg, Tag, Of>