Struct OptionalEnd 

pub struct OptionalEnd<C>(pub C);

Sugar for Optional(C, Eof).

Tuple Fields

0: C

Trait Implementations

impl<A, AST> ByteLen<Option<AST>> for OptionalEnd<A>

where A: ByteLen<AST>, AST: DeepView,

open spec fn exec_inv(&self) -> bool

{ self.0.exec_inv() }

exec fn length(&self, v: &Option<AST>) -> len : usize

impl<C: Clone> Clone for OptionalEnd<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<C> Consistency for OptionalEnd<C>

where C: Consistency,

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

{ Optional(self.0, super::Eof).consistent((v, ())) }

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

The type of values whose consistency is being checked.

impl<C: EquivSerializersGeneral> EquivSerializers for OptionalEnd<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<C: GoodSerializer> GoodSerializer for OptionalEnd<C>

open spec fn serialize_inv(&self) -> bool

{ self.0.serialize_inv() }

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

impl<C: MinMaxByteLen> MinMaxByteLen for OptionalEnd<C>

open spec fn min(&self) -> nat

{ Optional(self.0, super::Eof).min() }

open spec fn max(&self) -> nat

{ Optional(self.0, super::Eof).max() }

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

impl<C: NonMalleable + SafeParser> NonMalleable for OptionalEnd<C>

open spec fn nonmal_inv(&self) -> bool

{ Optional(self.0, super::Eof).nonmal_inv() }

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

impl<I, A> Parser<I> for OptionalEnd<A>

where I: InputBuf, A: 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 = Option<<A as Parser<I>>::PT>

Executable value returned by this parser.

impl<A, AST> Prepare<Option<AST>> for OptionalEnd<A>

where A: Prepare<AST>, AST: DeepView,

open spec fn exec_inv(&self) -> bool

{ self.0.exec_inv() }

exec fn prepare(&self, v: &Option<AST>) -> Result<usize, PreSerializeError>

impl<C: SafeParser> Productive for OptionalEnd<C>

open spec fn productive_inv(&self) -> bool

{ false }

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

impl<C: SPRoundTripDps + NonTailFmt + Productive> SPRoundTripDps for OptionalEnd<C>

open spec fn unambiguous(&self) -> bool

{
    &&& self.0.serialize_dps_inv()
    &&& self.0.unambiguous()
    &&& self.0.safe_inv()
    &&& self.0.productive_inv()

}

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

impl<C> SafeParser for OptionalEnd<C>

where C: SafeParser,

open spec fn safe_inv(&self) -> bool

{ self.0.safe_inv() }

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

impl<Output: OutputBuf, A, T> Serializer<Output, Option<T>> for OptionalEnd<A>

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

open spec fn exec_inv(&self) -> bool

{ self.0.exec_inv() }

exec fn serialize_into(&self, v: &Option<T>, obuf: &mut Output)

impl<C> SoundParser for OptionalEnd<C>

where C: 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<C: SpecByteLen> SpecByteLen for OptionalEnd<C>

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

{ Optional(self.0, super::Eof).byte_len((v, ())) }

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

The type of values whose byte length is being computed.

impl<C: SpecParser> SpecParser for OptionalEnd<C>

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

{
    match Optional(self.0, super::Eof).spec_parse(ibuf) {
        Some((n, (v, _))) => Some((n, v)),
        None => None,
    }
}

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

The type of parsed values.

impl<C: SpecSerializer> SpecSerializer for OptionalEnd<C>

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

{ Optional(self.0, super::Eof).spec_serialize((v, ())) }

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

The type of values to be serialized.

impl<C: SpecSerializerDps> SpecSerializerDps for OptionalEnd<C>

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

{ Optional(self.0, super::Eof).spec_serialize_dps((v, ()), obuf) }

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

The type of values to be serialized.

impl<C: ValueByteLen> ValueByteLen for OptionalEnd<C>

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

{ <Optional<C, super::Eof> as ValueByteLen>::value_byte_len((v, ())) }

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

impl<C: Copy> Copy for OptionalEnd<C>