Struct Array 

pub struct Array<const N: usize, C>(pub C);

Exactly N repetitions of combinator C (N is a compile-time constant).

Tuple Fields

0: C

Trait Implementations

impl<Inner, T, const N: usize> ByteLen<[T; N]> for Array<N, Inner>

where Inner: ByteLen<T>, T: DeepView,

open spec fn exec_inv(&self) -> bool

{ self.0.exec_inv() }

exec fn length(&self, v: &[T; N]) -> len : usize

impl<const N: usize, C: Clone> Clone for Array<N, C>

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

ensures

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

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

Performs copy-assignment from source.

impl<const N: usize, C: Consistency> Consistency for Array<N, C>

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

{ super::RepeatN(N, self.0).consistent(v) }

type Val = Seq<<C as Consistency>::Val>

The type of values whose consistency is being checked.

impl<const N: usize, C: EquivSerializersGeneral> EquivSerializers for Array<N, C>

open spec fn equiv_inv(&self) -> bool

{ self.0.equiv_general_inv() }

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

impl<const N: usize, C: EquivSerializersGeneral> EquivSerializersGeneral for Array<N, C>

open spec fn equiv_general_inv(&self) -> bool

{ self.0.equiv_general_inv() }

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

impl<const N: usize, C: GoodSerializer> GoodSerializer for Array<N, C>

open spec fn serialize_inv(&self) -> bool

{ super::RepeatN(N, self.0).serialize_inv() }

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

impl<const N: usize, C: MinMaxByteLen> MinMaxByteLen for Array<N, C>

open spec fn min(&self) -> nat

{ super::RepeatN(N, self.0).min() }

open spec fn max(&self) -> nat

{ super::RepeatN(N, self.0).max() }

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

impl<const N: usize, C: NoLookAhead> NoLookAhead for Array<N, C>

open spec fn no_lookahead_inv(&self) -> bool

{ self.0.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<const N: usize, C: NonMalleable> NonMalleable for Array<N, C>

open spec fn nonmal_inv(&self) -> bool

{ super::RepeatN(N, self.0).nonmal_inv() }

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

impl<const N: usize, C: NonTailFmt> NonTailFmt for Array<N, C>

open spec fn serialize_dps_inv(&self) -> bool

{ super::RepeatN(N, self.0).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, Inner, const N: usize> Parser<I> for Array<N, Inner>

where I: InputBuf, Inner: Parser<I> + SafeParser,

open spec fn exec_inv(&self) -> bool

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

}

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

type PT = [<Inner as Parser<I>>::PT; N]

Executable value returned by this parser.

impl<Inner, T, const N: usize> Prepare<[T; N]> for Array<N, Inner>

where Inner: Prepare<T>, T: DeepView,

open spec fn exec_inv(&self) -> bool

{ self.0.exec_inv() }

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

impl<const N: usize, C: Productive> Productive for Array<N, C>

open spec fn productive_inv(&self) -> bool

{ super::RepeatN(N, self.0).productive_inv() }

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

impl<const N: usize, C> SPRoundTripDps for Array<N, C>

where C: SPRoundTripDps + NonTailFmt,

open spec fn unambiguous(&self) -> bool

{ super::RepeatN(N, self.0).unambiguous() }

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

impl<const N: usize, C: SafeParser> SafeParser for Array<N, C>

open spec fn safe_inv(&self) -> bool

{ super::RepeatN(N, self.0).safe_inv() }

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

impl<Output: OutputBuf, Inner, T, const N: usize> Serializer<Output, [T; N]> for Array<N, Inner>

where T: DeepView, Inner: Serializer<Output, T>,

open spec fn exec_inv(&self) -> bool

{ self.0.exec_inv() }

exec fn serialize_into(&self, v: &[T; N], obuf: &mut Output)

impl<const N: usize, C: SoundParser> SoundParser for Array<N, C>

open spec fn sound_inv(&self) -> bool

{ super::RepeatN(N, self.0).sound_inv() }

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

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

impl<const N: usize, C: SpecByteLen> SpecByteLen for Array<N, C>

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

{ super::RepeatN(N, self.0).byte_len(v) }

type T = Seq<<C as SpecByteLen>::T>

The type of values whose byte length is being computed.

impl<const N: usize, C: SpecParser> SpecParser for Array<N, C>

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

{ super::RepeatN(N, self.0).spec_parse(ibuf) }

type PVal = Seq<<C as SpecParser>::PVal>

The type of parsed values.

impl<const N: usize, C: SpecSerializer> SpecSerializer for Array<N, C>

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

{ super::RepeatN(N, self.0).spec_serialize(v) }

type SVal = Seq<<C as SpecSerializer>::SVal>

The type of values to be serialized.

impl<const N: usize, C: SpecSerializerDps> SpecSerializerDps for Array<N, C>

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

{ super::RepeatN(N, self.0).spec_serialize_dps(v, obuf) }

type SValue = Seq<<C as SpecSerializerDps>::SValue>

The type of values to be serialized.

impl<const N: usize, C: StaticByteLen> StaticByteLen for Array<N, C>

open spec fn static_byte_len() -> nat

{ N as nat * C::static_byte_len() }

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

impl<const N: usize, C: ValueByteLen> ValueByteLen for Array<N, C>

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

{ <super::Star<C> as ValueByteLen>::value_byte_len(v) }

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

impl<const N: usize, C: Copy> Copy for Array<N, C>