Struct Eof 

pub struct Eof;

End-of-file combinator: denotes the “EOF”.

Parsing semantics: succeeds only if the input is empty, producing ().

Implements AdmitsUniqueVal.

Note

The DPS serialization always replaces the output buffer with the empty sequence, so Eof should only appear at the end of a format (and the trait system enforces this).

Trait Implementations

impl AdmitsUniqueVal for Eof

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

impl ByteLen<()> for Eof

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

fn exec_inv(&self) -> bool

impl Clone for Eof

fn clone(&self) -> Eof

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Consistency for Eof

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

{ true }

type Val = ()

The type of values whose consistency is being checked.

impl DerOrd<()> for Eof

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 Eof

type State = bool

impl EquivSerializers for Eof

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

fn equiv_inv(&self) -> bool

impl GoodSerializer for Eof

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

fn serialize_inv(&self) -> bool

impl HasAsn1Start for Eof

EOF accepts only the empty input.

open spec fn asn1_start(&self) -> Asn1StartDomain

{ asn1_start_empty() }

proof fn lemma_parse_implies_asn1_start(&self, input: Seq<u8>)

impl MinMaxByteLen for Eof

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 NonMalleable for Eof

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

fn nonmal_inv(&self) -> bool

impl<I: InputBuf> Parser<I> for Eof

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 Eof

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

fn exec_inv(&self) -> bool

impl Productive for Eof

open spec fn productive_inv(&self) -> bool

{ false }

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

impl SPRoundTripDps for Eof

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

fn unambiguous(&self) -> bool

impl SafeParser for Eof

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

fn safe_inv(&self) -> bool

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

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

fn exec_inv(&self) -> bool

impl SoundParser for Eof

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 Eof

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 Eof

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

{ if ibuf.len() == 0 { Some((0, ())) } else { None } }

type PVal = ()

The type of parsed values.

impl SpecSerializer for Eof

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 Eof

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

{ Seq::empty() }

type SValue = ()

The type of values to be serialized.

impl StaticByteLen for Eof

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 Eof

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)

impl Copy for Eof