Struct Star 

pub struct Star<A>(pub A);

Kleene star combinator: greedy zero-or-more repetition, consuming/producing Seq<A::PVal>.

Parsing semantics: always succeeds (may return an empty sequence). Stops when A fails or consumes zero bytes.

Consistency

A sequence s is consistent with Star<A> iff every element of s is consistent with A.

Note

This combinator is mostly used internally to specify Repeat<A, B>, which is able to disambiguate A and B and hence more compositional.

Tuple Fields

0: A

Implementations

impl<A: SpecParser> Star<A>

pub open spec fn parse_rec(&self, ibuf: Seq<u8>) -> (int, Seq<A::PVal>)

{
    match self.0.spec_parse(ibuf) {
        Some((n, v)) if 0 < n <= ibuf.len() => {
            let (n_rest, vs) = self.parse_rec(ibuf.skip(n));
            (n + n_rest, seq![v] + vs)
        }
        _ => (0, Seq::empty()),
    }
}

Recursive helper function for parsing. Since Star always succeeds, this function is total.

impl<A: SpecByteLen> Star<A>

pub proof fn lemma_byte_len_cons(&self, v: A::T, vs: Seq<A::T>)

ensures

self.byte_len(seq![v] + vs) == self.0.byte_len(v) + self.byte_len(vs),

impl<A: SpecSerializer + Copy> Star<A>

pub proof fn lemma_spec_serialize_cons(&self, first: A::SVal, rest: Seq<A::SVal>)

ensures

self.spec_serialize(seq![first] + rest)
    == self.0.spec_serialize(first) + self.spec_serialize(rest),

Serializing a nonempty sequence is the serialization of its first value followed by the serialization of the remaining values.

pub proof fn lemma_spec_serialize_suffix_step(&self, vs: Seq<A::SVal>, i: int)

requires

0 <= i < vs.len(),

ensures

self.spec_serialize(vs.skip(i))
    == self.0.spec_serialize(vs[i]) + self.spec_serialize(vs.skip(i + 1)),

Decomposes the serialization suffix beginning at i.

impl<A: SpecSerializerDps> Star<A>

pub open spec fn rfold_serialize_dps(&self, vs: Seq<A::SValue>, obuf: Seq<u8>) -> Seq<u8>

{ vs.fold_right_alt(|elem, buf| self.0.spec_serialize_dps(elem, buf), obuf) }

Trait Implementations

impl<Inner, T> ByteLen<[T]> for Star<Inner>

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

open spec fn exec_inv(&self) -> bool

{ self.0.exec_inv() }

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

impl<A: Clone> Clone for Star<A>

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

ensures

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

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

Performs copy-assignment from source.

impl<A> Consistency for Star<A>

where A: Consistency,

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

{ forall |i: int| 0 <= i < vs.len() ==> self.0.consistent(#[trigger] vs[i]) }

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

The type of values whose consistency is being checked.

impl<A, T> DerOrd<Vec<T>> for Star<A>

where T: DeepView, A: DerOrd<T> + Copy,

Available on crate feature alloc only.

proof fn lemma_der_serialize_len(&self, vs: Seq<T::V>)

open spec fn der_remaining(&self, vs: Seq<T::V>, state: StarDerState<A::State>) -> Seq<u8>

{
    if state.index < vs.len() {
        self.0.der_remaining(vs[state.index as int], state.current)
            + Star(self.0).spec_serialize(vs.skip(state.index as int + 1))
    } else {
        Seq::empty()
    }
}

open spec fn der_state_valid(&self, vs: Seq<T::V>, state: StarDerState<A::State>) -> bool

{
    &&& state.index <= vs.len()
    &&& state.index < vs.len()
        ==> { self.0.der_state_valid(vs[state.index as int], state.current) }

}

exec fn der_start(&self, v: &Vec<T>) -> state : StarDerState<A::State>

exec fn der_next(&self, v: &Vec<T>, state: &mut StarDerState<A::State>) -> next : Option<u8>

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

impl<A: DerState> DerState for Star<A>

type State = StarDerState<<A as DerState>::State>

impl<A> EquivSerializers for Star<A>

where A: EquivSerializersGeneral,

open spec fn equiv_inv(&self) -> bool

{ self.0.equiv_general_inv() }

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

impl<A> EquivSerializersGeneral for Star<A>

where A: EquivSerializersGeneral,

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<A: GoodSerializer> GoodSerializer for Star<A>

open spec fn serialize_inv(&self) -> bool

{ self.0.serialize_inv() }

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

impl<A: NonMalleable + SafeParser> NonMalleable for Star<A>

open spec fn nonmal_inv(&self) -> bool

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

}

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

impl<A> NonTailFmt for Star<A>

where A: NonTailFmt,

open spec fn serialize_dps_inv(&self) -> bool

{ self.0.serialize_dps_inv() }

proof fn lemma_serialize_dps_prepend(&self, vs: Self::SValue, obuf: Seq<u8>)

proof fn lemma_serialize_dps_len(&self, vs: Self::SValue, obuf: Seq<u8>)

impl<I, Inner> Parser<I> for Star<Inner>

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

Available on crate feature alloc only.

open spec fn exec_inv(&self) -> bool

{
    &&& self.0.exec_inv()
    &&& self.0.safe_inv()
    &&& self.0.productive_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, T> Prepare<[T]> for Star<Inner>

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

open spec fn exec_inv(&self) -> bool

{ self.0.exec_inv() }

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

impl<A: SafeParser> Productive for Star<A>

open spec fn productive_inv(&self) -> bool

{ false }

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

impl<A> SafeParser for Star<A>

where A: SafeParser,

open spec fn safe_inv(&self) -> bool

{ self.0.safe_inv() }

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

impl<Output: OutputBuf, Inner, T> Serializer<Output, [T]> for Star<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], obuf: &mut Output)

impl<A> SoundParser for Star<A>

where A: SoundParser,

open spec fn sound_inv(&self) -> bool

{ 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<A: SpecByteLen> SpecByteLen for Star<A>

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

{ v.fold_left(0, |acc: nat, elem| acc + self.0.byte_len(elem)) }

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

The type of values whose byte length is being computed.

impl<A: SpecParser> SpecParser for Star<A>

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

{
    let (n, vs) = self.parse_rec(ibuf);
    Some((n, vs))
}

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

The type of parsed values.

impl<A> SpecSerializer for Star<A>

where A: SpecSerializer,

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

{ spec_serialize_seq(&self.0, vs) }

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

The type of values to be serialized.

impl<A> SpecSerializerDps for Star<A>

where A: SpecSerializerDps,

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

{ self.rfold_serialize_dps(vs, obuf) }

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

The type of values to be serialized.

impl<A: ValueByteLen> ValueByteLen for Star<A>

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

{ v.fold_left(0, |acc: nat, elem| acc + A::value_byte_len(elem)) }

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

impl<A: Copy> Copy for Star<A>