Struct Permute5 

pub struct Permute5<A, B, C, D, E>(pub A, pub B, pub C, pub D, pub E);

Permute5<A, B, C, D, E> parses any permutation and produces (A::PVal, (B::PVal, (C::PVal, (D::PVal, E::PVal))))

Permute5(A, B, C, D, E) ::= Alt(
    (A, Permute4(B, C, D, E)),
    Alt(
        Mapped((B, Permute4(A, C, D, E)), swap5_1),
        Alt(
            Mapped((C, Permute4(A, B, D, E)), swap5_2),
            Alt(
                Mapped((D, Permute4(A, B, C, E)), swap5_3),
                Mapped((E, Permute4(A, B, C, D)), swap5_4),
            )
        )
    )
)

Tuple Fields

0: A

1: B

2: C

3: D

4: E

Trait Implementations

impl<A, B, C, D, E, TA, TB, TC, TD, TE> ByteLen<(TA, (TB, (TC, (TD, TE))))> for Permute5<A, B, C, D, E>

where TA: DeepView, TB: DeepView, TC: DeepView, TD: DeepView, TE: DeepView, A: ByteLen<TA>, B: ByteLen<TB>, C: ByteLen<TC>, D: ByteLen<TD>, E: ByteLen<TE>,

open spec fn exec_inv(&self) -> bool

{
    &&& self.0.exec_inv()
    &&& self.1.exec_inv()
    &&& self.2.exec_inv()
    &&& self.3.exec_inv()
    &&& self.4.exec_inv()

}

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

impl<A: Clone, B: Clone, C: Clone, D: Clone, E: Clone> Clone for Permute5<A, B, C, D, E>

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

ensures

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

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

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

call_ensures(D::clone, (&self.3,), cloned.3),

call_ensures(E::clone, (&self.4,), cloned.4),

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

Performs copy-assignment from source.

impl<A, B, C, D, E> Consistency for Permute5<A, B, C, D, E>

where A: Consistency, B: Consistency, C: Consistency, D: Consistency, E: Consistency,

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

{
    self.0.consistent(v.0) && self.1.consistent(v.1.0) && self.2.consistent(v.1.1.0)
        && self.3.consistent(v.1.1.1.0) && self.4.consistent(v.1.1.1.1)
}

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

The type of values whose consistency is being checked.

impl<A, B, C, D, E> EquivSerializers for Permute5<A, B, C, D, E>

where A: EquivSerializersGeneral, B: EquivSerializersGeneral, C: EquivSerializersGeneral, D: EquivSerializersGeneral, E: EquivSerializers,

open spec fn equiv_inv(&self) -> bool

{
    &&& self.0.equiv_general_inv()
    &&& self.1.equiv_general_inv()
    &&& self.2.equiv_general_inv()
    &&& self.3.equiv_general_inv()
    &&& self.4.equiv_inv()

}

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

impl<A, B, C, D, E> EquivSerializersGeneral for Permute5<A, B, C, D, E>

where A: EquivSerializersGeneral, B: EquivSerializersGeneral, C: EquivSerializersGeneral, D: EquivSerializersGeneral, E: EquivSerializersGeneral,

open spec fn equiv_general_inv(&self) -> bool

{
    &&& self.0.equiv_general_inv()
    &&& self.1.equiv_general_inv()
    &&& self.2.equiv_general_inv()
    &&& self.3.equiv_general_inv()
    &&& self.4.equiv_general_inv()

}

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

impl<A, B, C, D, E> GoodSerializer for Permute5<A, B, C, D, E>

where A: GoodSerializer, B: GoodSerializer, C: GoodSerializer, D: GoodSerializer, E: GoodSerializer,

open spec fn serialize_inv(&self) -> bool

{
    &&& self.0.serialize_inv()
    &&& self.1.serialize_inv()
    &&& self.2.serialize_inv()
    &&& self.3.serialize_inv()
    &&& self.4.serialize_inv()

}

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

impl<A: MinMaxByteLen, B: MinMaxByteLen, C: MinMaxByteLen, D: MinMaxByteLen, E: MinMaxByteLen> MinMaxByteLen for Permute5<A, B, C, D, E>

open spec fn min(&self) -> nat

{ Pair(self.0, super::Permute4(self.1, self.2, self.3, self.4)).min() }

open spec fn max(&self) -> nat

{ Pair(self.0, super::Permute4(self.1, self.2, self.3, self.4)).max() }

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

impl<A, B, C, D, E> NonTailFmt for Permute5<A, B, C, D, E>

where A: NonTailFmt, B: NonTailFmt, C: NonTailFmt, D: NonTailFmt, E: NonTailFmt,

open spec fn serialize_dps_inv(&self) -> bool

{
    &&& self.0.serialize_dps_inv()
    &&& self.1.serialize_dps_inv()
    &&& self.2.serialize_dps_inv()
    &&& self.3.serialize_dps_inv()
    &&& self.4.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, C, D, E> Parser<I> for Permute5<A, B, C, D, E>

where I: InputBuf, A: Parser<I> + SafeParser, B: Parser<I> + SafeParser, C: Parser<I> + SafeParser, D: Parser<I> + SafeParser, E: 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()
    &&& self.2.exec_inv()
    &&& self.2.safe_inv()
    &&& self.3.exec_inv()
    &&& self.3.safe_inv()
    &&& self.4.exec_inv()
    &&& self.4.safe_inv()

}

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

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

Executable value returned by this parser.

impl<A, B, C, D, E, TA, TB, TC, TD, TE> Prepare<(TA, (TB, (TC, (TD, TE))))> for Permute5<A, B, C, D, E>

where TA: DeepView, TB: DeepView, TC: DeepView, TD: DeepView, TE: DeepView, A: Prepare<TA>, B: Prepare<TB>, C: Prepare<TC>, D: Prepare<TD>, E: Prepare<TE>,

open spec fn exec_inv(&self) -> bool

{
    &&& self.0.exec_inv()
    &&& self.1.exec_inv()
    &&& self.2.exec_inv()
    &&& self.3.exec_inv()
    &&& self.4.exec_inv()

}

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

impl<A: Productive, B: Productive, C: Productive, D: Productive, E: Productive> Productive for Permute5<A, B, C, D, E>

open spec fn productive_inv(&self) -> bool

{
    &&& self.0.productive_inv()
    &&& self.1.productive_inv()
    &&& self.2.productive_inv()
    &&& self.3.productive_inv()
    &&& self.4.productive_inv()

}

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

impl<A, B, C, D, E> SPRoundTripDps for Permute5<A, B, C, D, E>

where A: SPRoundTripDps + NonTailFmt, B: SPRoundTripDps + NonTailFmt, C: SPRoundTripDps + NonTailFmt, D: SPRoundTripDps + NonTailFmt, E: SPRoundTripDps,

open spec fn unambiguous(&self) -> bool

{
    &&& self.0.unambiguous()
    &&& self.1.unambiguous()
    &&& self.2.unambiguous()
    &&& self.3.unambiguous()
    &&& self.4.unambiguous()
    &&& self.0.serialize_dps_inv()
    &&& self.1.serialize_dps_inv()
    &&& self.2.serialize_dps_inv()
    &&& self.3.serialize_dps_inv()

}

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

impl<A: SafeParser, B: SafeParser, C: SafeParser, D: SafeParser, E: SafeParser> SafeParser for Permute5<A, B, C, D, E>

open spec fn safe_inv(&self) -> bool

{
    &&& self.0.safe_inv()
    &&& self.1.safe_inv()
    &&& self.2.safe_inv()
    &&& self.3.safe_inv()
    &&& self.4.safe_inv()

}

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

impl<Output: OutputBuf, A, B, C, D, E, TA, TB, TC, TD, TE> Serializer<Output, (TA, (TB, (TC, (TD, TE))))> for Permute5<A, B, C, D, E>

where TA: DeepView, TB: DeepView, TC: DeepView, TD: DeepView, TE: DeepView, A: Serializer<Output, TA>, B: Serializer<Output, TB>, C: Serializer<Output, TC>, D: Serializer<Output, TD>, E: Serializer<Output, TE>,

open spec fn exec_inv(&self) -> bool

{
    &&& self.0.exec_inv()
    &&& self.1.exec_inv()
    &&& self.2.exec_inv()
    &&& self.3.exec_inv()
    &&& self.4.exec_inv()

}

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

impl<A: SoundParser, B: SoundParser, C: SoundParser, D: SoundParser, E: SoundParser> SoundParser for Permute5<A, B, C, D, E>

open spec fn sound_inv(&self) -> bool

{
    &&& self.0.sound_inv()
    &&& self.1.sound_inv()
    &&& self.2.sound_inv()
    &&& self.3.sound_inv()
    &&& self.4.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, C: SpecByteLen, D: SpecByteLen, E: SpecByteLen> SpecByteLen for Permute5<A, B, C, D, E>

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

{ Pair(self.0, super::Permute4(self.1, self.2, self.3, self.4)).byte_len(v) }

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

The type of values whose byte length is being computed.

impl<A, B, C, D, E> SpecParser for Permute5<A, B, C, D, E>

where A: SpecParser, B: SpecParser, C: SpecParser, D: SpecParser, E: SpecParser,

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

{
    let inner = Alt::<
        _,
        _,
        false,
    >(
        Pair(self.0, super::Permute4(self.1, self.2, self.3, self.4)),
        Alt::<
            _,
            _,
            false,
        >(
            Mapped {
                inner: Pair(self.1, super::Permute4(self.0, self.2, self.3, self.4)),
                mapper: |i| super::swap5_1(i),
            },
            Alt::<
                _,
                _,
                false,
            >(
                Mapped {
                    inner: Pair(self.2, super::Permute4(self.0, self.1, self.3, self.4)),
                    mapper: |i| super::swap5_2(i),
                },
                Alt::<
                    _,
                    _,
                    false,
                >(
                    Mapped {
                        inner: Pair(
                            self.3,
                            super::Permute4(self.0, self.1, self.2, self.4),
                        ),
                        mapper: |i| super::swap5_3(i),
                    },
                    Mapped {
                        inner: Pair(
                            self.4,
                            super::Permute4(self.0, self.1, self.2, self.3),
                        ),
                        mapper: |i| super::swap5_4(i),
                    },
                ),
            ),
        ),
    );
    inner.spec_parse(ibuf)
}

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

The type of parsed values.

impl<A, B, C, D, E> SpecSerializer for Permute5<A, B, C, D, E>

where A: SpecSerializer, B: SpecSerializer, C: SpecSerializer, D: SpecSerializer, E: SpecSerializer,

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

{ Pair(self.0, super::Permute4(self.1, self.2, self.3, self.4)).spec_serialize(v) }

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

The type of values to be serialized.

impl<A, B, C, D, E> SpecSerializerDps for Permute5<A, B, C, D, E>

where A: SpecSerializerDps, B: SpecSerializerDps, C: SpecSerializerDps, D: SpecSerializerDps, E: SpecSerializerDps,

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

{
    Pair(self.0, super::Permute4(self.1, self.2, self.3, self.4))
        .spec_serialize_dps(v, obuf)
}

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

The type of values to be serialized.

impl<A: StaticByteLen, B: StaticByteLen, C: StaticByteLen, D: StaticByteLen, E: StaticByteLen> StaticByteLen for Permute5<A, B, C, D, E>

open spec fn static_byte_len() -> nat

{
    A::static_byte_len()
        + <super::Permute4<B, C, D, E> as StaticByteLen>::static_byte_len()
}

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

impl<A: ValueByteLen, B: ValueByteLen, C: ValueByteLen, D: ValueByteLen, E: ValueByteLen> ValueByteLen for Permute5<A, B, C, D, E>

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

{
    <crate::combinators::Pair<
        A,
        super::Permute4<B, C, D, E>,
    > as ValueByteLen>::value_byte_len(v)
}

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

impl<A: Copy, B: Copy, C: Copy, D: Copy, E: Copy> Copy for Permute5<A, B, C, D, E>