Struct PairRev 

pub struct PairRev<A, B>(pub B, pub A);

Sequential composition of formats A and B, where the direction of parsing is reversed compared to super::Pair.

Parsing semantics: parses B from the back, consumes the tail part of the input, then parses A.

Tuple Fields

0: B

1: A

Trait Implementations

impl<A, B, AVal, BVal> ByteLen<(AVal, BVal)> for PairRev<A, B>

where AVal: DeepView, BVal: DeepView, A: ByteLen<AVal>, B: ByteLen<BVal>,

open spec fn exec_inv(&self) -> bool

{
    &&& self.0.exec_inv()
    &&& self.1.exec_inv()

}

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

impl<A: Clone, B: Clone> Clone for PairRev<A, B>

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

ensures

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

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

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

Performs copy-assignment from source.

impl<A, B> Consistency for PairRev<A, B>

where A: Consistency, B: Consistency,

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

{ Pair(self.1, self.0).consistent((v.0, v.1)) }

type Val = (<A as Consistency>::Val, <B as Consistency>::Val)

The type of values whose consistency is being checked.

impl<A, B> EquivSerializers for PairRev<A, B>

where A: EquivSerializersGeneral, B: EquivSerializers,

open spec fn equiv_inv(&self) -> bool

{ Pair(self.1, self.0).equiv_inv() }

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

impl<A, B> GoodSerializer for PairRev<A, B>

where A: GoodSerializer, B: GoodSerializer,

open spec fn serialize_inv(&self) -> bool

{ Pair(self.1, self.0).serialize_inv() }

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

impl<A: MinMaxByteLen, B: MinMaxByteLen> MinMaxByteLen for PairRev<A, B>

open spec fn min(&self) -> nat

{ self.1.min() + self.0.min() }

open spec fn max(&self) -> nat

{ self.1.max() + self.0.max() }

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

impl<A, B> NonMalleable for PairRev<A, B>

where A: NonMalleable, B: StaticByteLen + NonMalleable<PVal = B::T>,

open spec fn nonmal_inv(&self) -> bool

{
    &&& self.0.nonmal_inv()
    &&& self.1.nonmal_inv()
    &&& self.0.safe_inv()
    &&& self.1.safe_inv()

}

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

impl<A, B, AVal, BVal> Prepare<(AVal, BVal)> for PairRev<A, B>

where AVal: DeepView, BVal: DeepView, A: Prepare<AVal>, B: Prepare<BVal>,

open spec fn exec_inv(&self) -> bool

{
    &&& self.0.exec_inv()
    &&& self.1.exec_inv()

}

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

impl<A: Productive, B: StaticByteLen + SafeParser<PVal = B::T>> Productive for PairRev<A, B>

open spec fn productive_inv(&self) -> bool

{ B::static_byte_len() > 0 || (self.1.productive_inv() && self.1.safe_inv()) }

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

impl<A, B> SPRoundTripDps for PairRev<A, B>

where A: SPRoundTripDps + NonTailFmt + NoLookAhead, B: StaticByteLen + EquivSerializers + GoodSerializer + SPRoundTrip,

open spec fn unambiguous(&self) -> bool

{
    &&& self.0.serialize_inv()
    &&& self.0.equiv_inv()
    &&& self.0.sp_roundtrip_inv()
    &&& self.1.unambiguous()
    &&& self.1.serialize_dps_inv()
    &&& self.1.safe_inv()
    &&& self.1.no_lookahead_inv()

}

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

impl<A, B> SafeParser for PairRev<A, B>

where A: SafeParser, B: StaticByteLen + SafeParser<PVal = B::T>,

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

fn safe_inv(&self) -> bool

impl<A, B> SoundParser for PairRev<A, B>

where A: SoundParser, B: StaticByteLen + SoundParser,

open spec fn sound_inv(&self) -> bool

{
    &&& self.0.sound_inv()
    &&& self.1.sound_inv()

}

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

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

impl<A, B> SpecByteLen for PairRev<A, B>

where A: SpecByteLen, B: SpecByteLen,

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

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

type T = (<A as SpecByteLen>::T, <B as SpecByteLen>::T)

The type of values whose byte length is being computed.

impl<A, B> SpecParser for PairRev<A, B>

where A: SpecParser, B: StaticByteLen + SpecParser<PVal = B::T>,

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

{
    if ibuf.len() < B::static_byte_len() {
        None
    } else {
        let prefix = ibuf.len() - B::static_byte_len();
        match self.1.spec_parse(ibuf.take(prefix)) {
            Some((n1, v1)) if n1 == prefix => {
                match self.0.spec_parse(ibuf.skip(prefix)) {
                    Some((n2, v2)) if n2 == B::static_byte_len() => {
                        Some((n1 + n2, (v1, v2)))
                    }
                    _ => None,
                }
            }
            _ => None,
        }
    }
}

type PVal = (<A as SpecParser>::PVal, <B as SpecParser>::PVal)

The type of parsed values.

impl<A, B> SpecSerializer for PairRev<A, B>

where A: SpecSerializer, B: SpecSerializer,

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

{ Pair(self.1, self.0).spec_serialize((v.0, v.1)) }

type SVal = (<A as SpecSerializer>::SVal, <B as SpecSerializer>::SVal)

The type of values to be serialized.

impl<A, B> SpecSerializerDps for PairRev<A, B>

where A: SpecSerializerDps, B: SpecSerializerDps,

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

{ self.1.spec_serialize_dps(v.0, self.0.spec_serialize_dps(v.1, seq![])) }

type SValue = (<A as SpecSerializerDps>::SValue, <B as SpecSerializerDps>::SValue)

The type of values to be serialized.

impl<A, B> StaticByteLen for PairRev<A, B>

where A: StaticByteLen, B: StaticByteLen,

open spec fn static_byte_len() -> nat

{ A::static_byte_len() + B::static_byte_len() }

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

impl<A, B> ValueByteLen for PairRev<A, B>

where A: ValueByteLen, B: ValueByteLen,

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

{ A::value_byte_len(v.0) + B::value_byte_len(v.1) }

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

impl<A: Copy, B: Copy> Copy for PairRev<A, B>