Struct Tail 

pub struct Tail;

Tail combinator: denotes the “tail” of the format, useful for under-specification.

Parsing semantics: consumes and return all remaining bytes (even if the input is empty).

Note

The DPS serialization replaces (not prepends to) the output buffer, so Tail should only appear at the end of a format (and the trait system enforces this).

Trait Implementations

impl<'i> ByteLen<&'i [u8]> for Tail

open spec fn exec_inv(&self) -> bool

{ true }

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

impl ByteLen<[u8]> for Tail

open spec fn exec_inv(&self) -> bool

{ true }

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

impl BytesCombinator for Tail

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

impl Clone for Tail

fn clone(&self) -> Tail

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Consistency for Tail

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

{ true }

type Val = Seq<u8>

The type of values whose consistency is being checked.

impl Copy for Tail

impl<'a> DerOrd<&'a [u8]> for Tail

proof fn lemma_der_serialize_len(&self, value: Seq<u8>)

open spec fn der_remaining(&self, value: Seq<u8>, state: BytesDerState) -> Seq<u8>

{ value[state.pos..] }

open spec fn der_state_valid(&self, value: Seq<u8>, state: BytesDerState) -> bool

{ state.pos <= value.len() }

exec fn der_start(&self, b: &&'a [u8]) -> state : BytesDerState

exec fn der_next(&self, b: &&'a [u8], state: &mut BytesDerState) -> next : Option<u8>

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

impl DerOrd<[u8]> for Tail

proof fn lemma_der_serialize_len(&self, value: Seq<u8>)

open spec fn der_remaining(&self, value: Seq<u8>, state: BytesDerState) -> Seq<u8>

{ value[state.pos..] }

open spec fn der_state_valid(&self, value: Seq<u8>, state: BytesDerState) -> bool

{ state.pos <= value.len() }

exec fn der_start(&self, b: &[u8]) -> state : BytesDerState

exec fn der_next(&self, b: &[u8], state: &mut BytesDerState) -> next : Option<u8>

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

impl DerState for Tail

type State = BytesDerState

impl EquivSerializers for Tail

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

fn equiv_inv(&self) -> bool

impl GoodSerializer for Tail

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

fn serialize_inv(&self) -> bool

impl NonMalleable for Tail

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

fn nonmal_inv(&self) -> bool

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

exec fn min_byte_len(&self) -> usize

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

type PT = I

Executable value returned by this parser.

fn exec_inv(&self) -> bool

impl<'i> Prepare<&'i [u8]> for Tail

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

fn exec_inv(&self) -> bool

impl Prepare<[u8]> for Tail

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

fn exec_inv(&self) -> bool

impl Productive for Tail

open spec fn productive_inv(&self) -> bool

{ false }

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

impl SPRoundTripDps for Tail

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

fn unambiguous(&self) -> bool

impl SafeParser for Tail

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

fn safe_inv(&self) -> bool

impl<'i, Output: OutputBuf> Serializer<Output, &'i [u8]> for Tail

exec fn serialize_into(&self, v: &&'i [u8], obuf: &mut Output)

fn exec_inv(&self) -> bool

impl<Output: OutputBuf> Serializer<Output, [u8]> for Tail

exec fn serialize_into(&self, v: &[u8], obuf: &mut Output)

fn exec_inv(&self) -> bool

impl SoundParser for Tail

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 Tail

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

{ v.len() }

type T = Seq<u8>

The type of values whose byte length is being computed.

impl SpecParser for Tail

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

{ Some((ibuf.len() as int, ibuf)) }

type PVal = Seq<u8>

The type of parsed values.

impl SpecSerializer for Tail

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

{ v }

type SVal = Seq<u8>

The type of values to be serialized.

impl SpecSerializerDps for Tail

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

{ v }

type SValue = Seq<u8>

The type of values to be serialized.

impl ValueByteLen for Tail

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

{ v.len() }

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