Struct Empty 

pub struct Empty;

Marker combinator that denotes the “empty” format.

Parsing semantics: always succeeds without consuming any input, returning ().

Serialization semantics: produces an empty byte sequence.

Trait Implementations

impl AdmitsUniqueVal for Empty

proof fn lemma_unique_consistent_val(&self, v1: Self::Val, v2: Self::Val)

impl ByteLen<()> for Empty

exec fn length(&self, _v: &()) -> len : usize

fn exec_inv(&self) -> bool

impl Clone for Empty

fn clone(&self) -> Empty

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Consistency for Empty

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

{ true }

type Val = ()

The type of values whose consistency is being checked.

impl Copy for Empty

impl DerOrd<()> for Empty

proof fn lemma_der_serialize_len(&self, _value: ())

open spec fn der_remaining(&self, _value: (), _state: bool) -> Seq<u8>

{ Seq::empty() }

open spec fn der_state_valid(&self, _value: (), _state: bool) -> bool

{ true }

exec fn der_start(&self, _v: &()) -> state : bool

exec fn der_next(&self, _v: &(), _state: &mut bool) -> next : Option<u8>

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

impl DerState for Empty

type State = bool

impl EquivSerializers for Empty

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

fn equiv_inv(&self) -> bool

impl EquivSerializersGeneral for Empty

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

fn equiv_general_inv(&self) -> bool

impl GoodSerializer for Empty

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

fn serialize_inv(&self) -> bool

impl LeafNonMalleable for Empty

proof fn nonmal_leaf_inv(&self)

impl MinMaxByteLen for Empty

open spec fn min(&self) -> nat

{ ZERO_BYTE_LEN as nat }

open spec fn max(&self) -> nat

{ ZERO_BYTE_LEN as nat }

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

impl NoLookAhead for Empty

proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>)

fn no_lookahead_inv(&self) -> bool

fn corollary_non_extensible(&self, i1: Seq<u8>, i2: Seq<u8>)

impl NonMalleable for Empty

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

fn nonmal_inv(&self) -> bool

impl NonTailFmt for Empty

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>)

fn serialize_dps_inv(&self) -> bool

impl<I: View<V = Seq<u8>>> Parser<I> for Empty

exec fn min_byte_len(&self) -> usize

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

type PT = ()

Executable value returned by this parser.

fn exec_inv(&self) -> bool

impl Prepare<()> for Empty

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

fn exec_inv(&self) -> bool

impl Productive for Empty

open spec fn productive_inv(&self) -> bool

{ false }

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

impl SPRoundTripDps for Empty

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

fn unambiguous(&self) -> bool

impl SafeParser for Empty

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

fn safe_inv(&self) -> bool

impl<Output: OutputBuf> Serializer<Output, ()> for Empty

exec fn serialize_into(&self, _v: &(), _obuf: &mut Output)

fn exec_inv(&self) -> bool

impl SoundParser for Empty

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

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

fn sound_inv(&self) -> bool

impl SpecByteLen for Empty

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

{ ZERO_BYTE_LEN as nat }

type T = ()

The type of values whose byte length is being computed.

impl SpecParser for Empty

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

{ Some((0, ())) }

type PVal = ()

The type of parsed values.

impl SpecSerializer for Empty

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

{ Seq::empty() }

type SVal = ()

The type of values to be serialized.

impl SpecSerializerDps for Empty

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

{ obuf }

type SValue = ()

The type of values to be serialized.

impl StaticByteLen for Empty

open spec fn static_byte_len() -> nat

{ ZERO_BYTE_LEN as nat }

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

impl ValueByteLen for Empty

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

{ ZERO_BYTE_LEN as nat }

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