Struct Opt 

pub struct Opt<A>(pub A);

Optional combinator: denotes an optional field.

Parsing semantics: tries A, returning Some(a) on success; on failure, returns None without consuming input.

Serialization semantics: if the value is Some(a), serializes a with A; if the value is None, produces no output.

Consistency

A value v is consistent with Opt<A> iff either v is consistent with A or v is None.

Note

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

Tuple Fields

0: A

Trait Implementations

impl<A, T> ByteLen<Option<T>> for Opt<A>

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

open spec fn exec_inv(&self) -> bool

{ self.0.exec_inv() }

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

impl<A: Clone> Clone for Opt<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 Opt<A>

where A: Consistency,

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

{
    match v {
        None => true,
        Some(vv) => self.0.consistent(vv),
    }
}

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

The type of values whose consistency is being checked.

impl<A, T> DerOrd<Option<T>> for Opt<A>

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

proof fn lemma_der_serialize_len(&self, value: Option<T::V>)

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

{
    match (value, state) {
        (Some(value), OptDerState::Some(state)) => self.0.der_remaining(value, state),
        (None, OptDerState::None) => Seq::empty(),
        _ => Seq::empty(),
    }
}

open spec fn der_state_valid( &self, value: Option<T::V>, state: OptDerState<A::State>, ) -> bool

{
    match (value, state) {
        (Some(value), OptDerState::Some(state)) => self.0.der_state_valid(value, state),
        (None, OptDerState::None) => true,
        _ => false,
    }
}

exec fn der_start(&self, o: &Option<T>) -> state : OptDerState<A::State>

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

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

impl<A: DerState> DerState for Opt<A>

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

impl<A> EquivSerializers for Opt<A>

where A: EquivSerializers,

open spec fn equiv_inv(&self) -> bool

{ self.0.equiv_inv() }

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

impl<A> EquivSerializersGeneral for Opt<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 Opt<A>

open spec fn serialize_inv(&self) -> bool

{ self.0.serialize_inv() }

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

impl<Inner: MinMaxByteLen> MinMaxByteLen for Opt<Inner>

open spec fn min(&self) -> nat

{ 0 }

open spec fn max(&self) -> nat

{ self.0.max() }

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

impl<A: NonMalleable> NonMalleable for Opt<A>

open spec fn nonmal_inv(&self) -> bool

{ self.0.nonmal_inv() }

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

impl<A> NonTailFmt for Opt<A>

where A: NonTailFmt,

open spec fn serialize_dps_inv(&self) -> bool

{ 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, A> Parser<I> for Opt<A>

where I: View<V = Seq<u8>>, A: Parser<I>,

open spec fn exec_inv(&self) -> bool

{ self.0.exec_inv() }

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

type PT = Option<<A as Parser<I>>::PT>

Executable value returned by this parser.

impl<A, T> Prepare<Option<T>> for Opt<A>

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

open spec fn exec_inv(&self) -> bool

{ self.0.exec_inv() }

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

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

open spec fn productive_inv(&self) -> bool

{ false }

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

impl<A> SafeParser for Opt<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, A, T> Serializer<Output, Option<T>> for Opt<A>

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

open spec fn exec_inv(&self) -> bool

{ self.0.exec_inv() }

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

impl<A> SoundParser for Opt<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<Inner: SpecByteLen> SpecByteLen for Opt<Inner>

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

{
    match v {
        None => 0,
        Some(vv) => self.0.byte_len(vv),
    }
}

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

The type of values whose byte length is being computed.

impl<A> SpecParser for Opt<A>

where A: SpecParser,

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

{
    match self.0.spec_parse(ibuf) {
        Some((n, v)) => Some((n, Some(v))),
        None => Some((0, None)),
    }
}

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

The type of parsed values.

impl<A> SpecSerializer for Opt<A>

where A: SpecSerializer,

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

{
    match v {
        None => Seq::empty(),
        Some(vv) => self.0.spec_serialize(vv),
    }
}

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

The type of values to be serialized.

impl<A> SpecSerializerDps for Opt<A>

where A: SpecSerializerDps,

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

{
    match v {
        None => obuf,
        Some(vv) => self.0.spec_serialize_dps(vv, obuf),
    }
}

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

The type of values to be serialized.

impl<Inner: ValueByteLen> ValueByteLen for Opt<Inner>

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

{
    match v {
        None => 0,
        Some(vv) => Inner::value_byte_len(vv),
    }
}

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

impl<A: Copy> Copy for Opt<A>