Struct Permute4 

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

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

Permute4(A, B, C, D) ::= Alt(
    (A, Permute3(B, C, D)),
    Alt(
        Mapped((B, Permute3(A, C, D)), swap4_1),
        Alt(
            Mapped((C, Permute3(A, B, D)), swap4_2),
            Mapped((D, Permute3(A, B, C)), swap4_3),
        )
    )
)

Tuple Fields

0: A

1: B

2: C

3: D

Trait Implementations

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

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

open spec fn exec_inv(&self) -> bool

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

}

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

impl<A: Clone, B: Clone, C: Clone, D: Clone> Clone for Permute4<A, B, C, D>

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),

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

Performs copy-assignment from source.

impl<A, B, C, D> Consistency for Permute4<A, B, C, D>

where A: Consistency, B: Consistency, C: Consistency, D: 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)
}

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

The type of values whose consistency is being checked.

impl<A, B, C, D> EquivSerializers for Permute4<A, B, C, D>

where A: EquivSerializersGeneral, B: EquivSerializersGeneral, C: EquivSerializersGeneral, D: 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_inv()

}

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

impl<A, B, C, D> EquivSerializersGeneral for Permute4<A, B, C, D>

where A: EquivSerializersGeneral, B: EquivSerializersGeneral, C: EquivSerializersGeneral, D: 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()

}

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

impl<A, B, C, D> GoodSerializer for Permute4<A, B, C, D>

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

open spec fn serialize_inv(&self) -> bool

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

}

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

impl<A: MinMaxByteLen, B: MinMaxByteLen, C: MinMaxByteLen, D: MinMaxByteLen> MinMaxByteLen for Permute4<A, B, C, D>

open spec fn min(&self) -> nat

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

open spec fn max(&self) -> nat

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

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

impl<A, B, C, D> NonTailFmt for Permute4<A, B, C, D>

where A: NonTailFmt, B: NonTailFmt, C: NonTailFmt, D: 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()

}

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> Parser<I> for Permute4<A, B, C, D>

where I: InputBuf, A: Parser<I> + SafeParser, B: Parser<I> + SafeParser, C: Parser<I> + SafeParser, D: 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()

}

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)))

Executable value returned by this parser.

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

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

open spec fn exec_inv(&self) -> bool

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

}

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

impl<A: Productive, B: Productive, C: Productive, D: Productive> Productive for Permute4<A, B, C, D>

open spec fn productive_inv(&self) -> bool

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

}

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

impl<A, B, C, D> SPRoundTripDps for Permute4<A, B, C, D>

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

open spec fn unambiguous(&self) -> bool

{
    &&& self.0.unambiguous()
    &&& self.1.unambiguous()
    &&& self.2.unambiguous()
    &&& self.3.unambiguous()
    &&& self.0.serialize_dps_inv()
    &&& self.1.serialize_dps_inv()
    &&& self.2.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> SafeParser for Permute4<A, B, C, D>

open spec fn safe_inv(&self) -> bool

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

}

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

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

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

open spec fn exec_inv(&self) -> bool

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

}

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

impl<A: SoundParser, B: SoundParser, C: SoundParser, D: SoundParser> SoundParser for Permute4<A, B, C, D>

open spec fn sound_inv(&self) -> bool

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

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

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

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

The type of values whose byte length is being computed.

impl<A, B, C, D> SpecParser for Permute4<A, B, C, D>

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

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

{
    let inner = Alt::<
        _,
        _,
        false,
    >(
        Pair(self.0, super::Permute3(self.1, self.2, self.3)),
        Alt::<
            _,
            _,
            false,
        >(
            Mapped {
                inner: Pair(self.1, super::Permute3(self.0, self.2, self.3)),
                mapper: |i| super::swap4_1(i),
            },
            Alt::<
                _,
                _,
                false,
            >(
                Mapped {
                    inner: Pair(self.2, super::Permute3(self.0, self.1, self.3)),
                    mapper: |i| super::swap4_2(i),
                },
                Mapped {
                    inner: Pair(self.3, super::Permute3(self.0, self.1, self.2)),
                    mapper: |i| super::swap4_3(i),
                },
            ),
        ),
    );
    inner.spec_parse(ibuf)
}

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

The type of parsed values.

impl<A, B, C, D> SpecSerializer for Permute4<A, B, C, D>

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

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

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

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

The type of values to be serialized.

impl<A, B, C, D> SpecSerializerDps for Permute4<A, B, C, D>

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

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

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

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

The type of values to be serialized.

impl<A: StaticByteLen, B: StaticByteLen, C: StaticByteLen, D: StaticByteLen> StaticByteLen for Permute4<A, B, C, D>

open spec fn static_byte_len() -> nat

{ A::static_byte_len() + <super::Permute3<B, C, D> 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> ValueByteLen for Permute4<A, B, C, D>

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

{
    <crate::combinators::Pair<
        A,
        super::Permute3<B, C, D>,
    > 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> Copy for Permute4<A, B, C, D>