Struct Pair 

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

Sequential composition of formats A and B.

Tuple Fields

0: A

1: B

Trait Implementations

impl<A, B, TA, TB> ByteLen<(TA, TB)> for Pair<A, B>

where TA: DeepView, TB: DeepView, A: ByteLen<TA>, B: ByteLen<TB>,

open spec fn exec_inv(&self) -> bool

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

}

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

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

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

ensures

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

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

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

Performs copy-assignment from source.

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

where A: Consistency, B: Consistency,

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

{ self.0.consistent(v.0) && self.1.consistent(v.1) }

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

The type of values whose consistency is being checked.

impl<D1: DepCombinator, D2: DepCombinator> DepCombinator for Pair<D1, D2>

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

{ Pair(self.0.apply(key.0), self.1.apply(key.1)) }

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

{ (self.0.recover(value.0), self.1.recover(value.1)) }

open spec fn recover_inv(&self) -> bool

{ self.0.recover_inv() && self.1.recover_inv() }

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

type Key = (<D1 as DepCombinator>::Key, <D2 as DepCombinator>::Key)

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

type Val = (<D1 as DepCombinator>::Val, <D2 as DepCombinator>::Val)

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

type Body = Pair<<D1 as DepCombinator>::Body, <D2 as DepCombinator>::Body>

The type of the body combinator produced by apply.

impl<A, B, TA, TB> DerOrd<(TA, TB)> for Pair<A, B>

where TA: DeepView, TB: DeepView, A: DerOrd<TA>, B: DerOrd<TB>,

proof fn lemma_der_serialize_len(&self, value: (TA::V, TB::V))

open spec fn der_remaining( &self, value: (TA::V, TB::V), state: PairDerState<A::State, B::State>, ) -> Seq<u8>

{
    if state.in_left {
        self.0.der_remaining(value.0, state.left)
            + self.1.der_remaining(value.1, state.right)
    } else {
        self.1.der_remaining(value.1, state.right)
    }
}

open spec fn der_state_valid( &self, value: (TA::V, TB::V), state: PairDerState<A::State, B::State>, ) -> bool

{
    &&& self.0.der_state_valid(value.0, state.left)
    &&& self.1.der_state_valid(value.1, state.right)
    &&& !state.in_left ==> self.0.der_remaining(value.0, state.left).len() == 0

}

exec fn der_start(&self, v: &(TA, TB)) -> state : PairDerState<A::State, B::State>

exec fn der_next( &self, v: &(TA, TB), state: &mut PairDerState<A::State, B::State>, ) -> next : Option<u8>

fn der_leq(&self, left: &T, right: &T) -> bool

impl<A: DerState, B: DerState> DerState for Pair<A, B>

type State = PairDerState<<A as DerState>::State, <B as DerState>::State>

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

where A: EquivSerializersGeneral, B: EquivSerializers,

open spec fn equiv_inv(&self) -> bool

{
    &&& self.0.equiv_general_inv()
    &&& self.1.equiv_inv()

}

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

impl<A, B> EquivSerializersGeneral for Pair<A, B>

where A: EquivSerializersGeneral, B: EquivSerializersGeneral,

open spec fn equiv_general_inv(&self) -> bool

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

}

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

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

where A: GoodSerializer, B: GoodSerializer,

open spec fn serialize_inv(&self) -> bool

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

}

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

impl<Left: HasAsn1Start, Right: SpecParser> HasAsn1Start for Pair<Left, Right>

A required pair starts wherever its required left component starts.

open spec fn asn1_start(&self) -> Asn1StartDomain

{ self.0.asn1_start() }

proof fn lemma_parse_implies_asn1_start(&self, input: Seq<u8>)

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

open spec fn max(&self) -> nat

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

open spec fn min(&self) -> nat

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

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

impl<A: NoLookAhead, B: NoLookAhead> NoLookAhead for Pair<A, B>

open spec fn no_lookahead_inv(&self) -> bool

{
    &&& self.0.no_lookahead_inv()
    &&& self.1.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<A: NonMalleable, B: NonMalleable> NonMalleable for Pair<A, B>

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> NonTailFmt for Pair<A, B>

where A: NonTailFmt, B: NonTailFmt,

open spec fn serialize_dps_inv(&self) -> bool

{
    &&& self.0.serialize_dps_inv()
    &&& self.1.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, A, B> Parser<I> for Pair<A, B>

where I: InputBuf, A: Parser<I> + SafeParser, B: Parser<I> + SafeParser,

open spec fn exec_inv(&self) -> bool

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

}

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

type PT = (<A as Parser<I>>::PT, <B as Parser<I>>::PT)

Executable value returned by this parser.

impl<A, B, TA, TB> Prepare<(TA, TB)> for Pair<A, B>

where TA: DeepView, TB: DeepView, A: Prepare<TA>, B: Prepare<TB>,

open spec fn exec_inv(&self) -> bool

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

}

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

impl<A: Productive, B: Productive> Productive for Pair<A, B>

open spec fn productive_inv(&self) -> bool

{
    ||| self.0.productive_inv()
    ||| self.1.productive_inv()

}

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

impl<A: SPRoundTripDps + NonTailFmt, B: SPRoundTripDps> SPRoundTripDps for Pair<A, B>

open spec fn unambiguous(&self) -> bool

{
    &&& self.0.serialize_dps_inv()
    &&& self.0.unambiguous()
    &&& self.1.unambiguous()

}

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

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

where A: SafeParser, B: SafeParser,

open spec fn safe_inv(&self) -> bool

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

}

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

impl<Output: OutputBuf, A, B, TA, TB> Serializer<Output, (TA, TB)> for Pair<A, B>

where TA: DeepView, TB: DeepView, A: Serializer<Output, TA>, B: Serializer<Output, TB>,

open spec fn exec_inv(&self) -> bool

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

}

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

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

where A: SoundParser, B: 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: SpecByteLen, B: SpecByteLen> SpecByteLen for Pair<A, B>

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

{ self.0.byte_len(v.0) + self.1.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 Pair<A, B>

where A: SpecParser, B: SpecParser,

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

{
    match self.0.spec_parse(ibuf) {
        Some((n1, v1)) => {
            match self.1.spec_parse(ibuf.skip(n1)) {
                Some((n2, v2)) => Some((n1 + n2, (v1, v2))),
                None => None,
            }
        }
        None => None,
    }
}

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

The type of parsed values.

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

where A: SpecSerializer, B: SpecSerializer,

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

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

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

The type of values to be serialized.

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

where A: SpecSerializerDps, B: SpecSerializerDps,

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

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

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

The type of values to be serialized.

impl<A: StaticByteLen, B: StaticByteLen> StaticByteLen for Pair<A, B>

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: ValueByteLen, B: ValueByteLen> ValueByteLen for Pair<A, B>

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 Pair<A, B>