Struct RepeatN 

pub struct RepeatN<C, N = u8>(pub N, pub C);

Exactly N repetitions of combinator C (N is a runtime value).

Tuple Fields

0: N

1: C

Implementations

impl<C: SpecParser, N: AsLen> RepeatN<C, N>

pub open spec fn parse_n_rec( &self, count: nat, ibuf: Seq<u8>, ) -> Option<(int, Seq<C::PVal>)>

{
    if count == 0 {
        Some((0, Seq::empty()))
    } else {
        match self.1.spec_parse(ibuf) {
            Some((n0, v0)) => {
                match self.parse_n_rec((count - 1) as nat, ibuf.skip(n0)) {
                    Some((n1, vs1)) => Some((n0 + n1, seq![v0] + vs1)),
                    None => None,
                }
            }
            None => None,
        }
    }
}

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

ensures

self.spec_parse(ibuf) matches Some((_, vs)) ==> vs.len() == self.0.as_nat(),

Trait Implementations

impl<Inner, N, T> ByteLen<[T]> for RepeatN<Inner, N>

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

open spec fn exec_inv(&self) -> bool

{ self.1.exec_inv() }

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

impl<C: Clone, N: Clone> Clone for RepeatN<C, N>

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

ensures

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

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

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

Performs copy-assignment from source.

impl<C: Consistency, N: AsLen> Consistency for RepeatN<C, N>

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

{
    &&& vs.len() == self.0.as_nat()
    &&& super::Star(self.1).consistent(vs)

}

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

The type of values whose consistency is being checked.

impl<C: EquivSerializersGeneral, N: AsLen> EquivSerializers for RepeatN<C, N>

open spec fn equiv_inv(&self) -> bool

{ self.1.equiv_general_inv() }

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

impl<C: EquivSerializersGeneral, N: AsLen> EquivSerializersGeneral for RepeatN<C, N>

open spec fn equiv_general_inv(&self) -> bool

{ self.1.equiv_general_inv() }

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

impl<C: GoodSerializer, N: AsLen> GoodSerializer for RepeatN<C, N>

open spec fn serialize_inv(&self) -> bool

{ self.1.serialize_inv() }

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

impl<C: MinMaxByteLen, N: AsLen> MinMaxByteLen for RepeatN<C, N>

open spec fn min(&self) -> nat

{ self.0.as_nat() * self.1.min() }

open spec fn max(&self) -> nat

{ self.0.as_nat() * self.1.max() }

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

impl<C: NoLookAhead, N: AsLen> NoLookAhead for RepeatN<C, N>

open spec fn no_lookahead_inv(&self) -> bool

{ 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<C: NonMalleable + SafeParser, N: AsLen> NonMalleable for RepeatN<C, N>

open spec fn nonmal_inv(&self) -> bool

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

}

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

impl<C: NonTailFmt, N: AsLen> NonTailFmt for RepeatN<C, N>

open spec fn serialize_dps_inv(&self) -> bool

{ 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, Inner, N> Parser<I> for RepeatN<Inner, N>

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

Available on crate feature alloc only.

open spec fn exec_inv(&self) -> bool

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

}

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

type PT = Vec<<Inner as Parser<I>>::PT>

Executable value returned by this parser.

impl<Inner, N, T> Prepare<[T]> for RepeatN<Inner, N>

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

open spec fn exec_inv(&self) -> bool

{ self.1.exec_inv() }

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

impl<C: Productive, N: AsLen> Productive for RepeatN<C, N>

open spec fn productive_inv(&self) -> bool

{
    &&& self.0.as_nat() > 0
    &&& self.1.productive_inv()

}

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

impl<C, N> SPRoundTripDps for RepeatN<C, N>

where C: SPRoundTripDps + NonTailFmt, N: AsLen,

open spec fn unambiguous(&self) -> bool

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

}

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

impl<C: SafeParser, N: AsLen> SafeParser for RepeatN<C, N>

open spec fn safe_inv(&self) -> bool

{ self.1.safe_inv() }

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

impl<Output: OutputBuf, Inner, N, T> Serializer<Output, [T]> for RepeatN<Inner, N>

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

open spec fn exec_inv(&self) -> bool

{ self.1.exec_inv() }

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

impl<C: SoundParser, N: AsLen> SoundParser for RepeatN<C, N>

open spec fn sound_inv(&self) -> bool

{ 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<C: SpecByteLen, N: AsLen> SpecByteLen for RepeatN<C, N>

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

{ super::Star(self.1).byte_len(vs) }

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

The type of values whose byte length is being computed.

impl<C: SpecParser, N: AsLen> SpecParser for RepeatN<C, N>

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

{ self.parse_n_rec(self.0.as_nat(), ibuf) }

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

The type of parsed values.

impl<C: SpecSerializer, N: AsLen> SpecSerializer for RepeatN<C, N>

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

{ spec_serialize_seq(&self.1, vs) }

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

The type of values to be serialized.

impl<C: SpecSerializerDps, N: AsLen> SpecSerializerDps for RepeatN<C, N>

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

{ super::Star(self.1).spec_serialize_dps(vs, obuf) }

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

The type of values to be serialized.

impl<C: ValueByteLen, N: AsLen> ValueByteLen for RepeatN<C, N>

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

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

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

impl<C: Copy, N: Copy> Copy for RepeatN<C, N>