Tail

vest_lib::regular::bytes

Struct Tail

pub struct Tail;

Expand description

Combinator that returns the rest of the input bytes from the current position.

Trait Implementations§

impl Clone for Tail

exec fn clone(&self) -> out : Self

ensures

out == *self,

1.0.0 · Source§

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

Performs copy-assignment from source. Read more

impl<'x, I: VestInput + 'x, O: VestOutput<I>> Combinator<'x, I, O> for Tail

exec fn length(&self, v: Self::SType) -> usize

exec fn parse(&self, s: I) -> res : Result<(usize, Self::Type), ParseError>

exec fn serialize( &self, v: Self::SType, data: &mut O, pos: usize, ) -> res : Result<usize, SerializeError>

type Type = I

The result type of parsing

type SType = &'x I

The input type of serialization, often a reference to Self::Type. For “structural” formats though (e.g., crate::regular::sequence::Pair and crate::regular::variant::Choice), this is the tuple/sum of the corresponding Combinator::SType types.

fn ex_requires(&self) -> bool

impl SecureSpecCombinator for Tail

proof fn theorem_serialize_parse_roundtrip(&self, v: Self::Type)

proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>)

open spec fn is_prefix_secure() -> bool

{ false }

proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>)

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

open spec fn is_productive(&self) -> bool

{ false }

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

fn corollary_parse_surjective(&self, v: Self::Type)

fn corollary_serialize_injective(&self, v1: Self::Type, v2: Self::Type)

fn corollary_serialize_injective_contraposition( &self, v1: Self::Type, v2: Self::Type, )

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

fn lemma_serialize_productive(&self, v: Self::Type)

impl SpecCombinator for Tail

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

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

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

{ v }

type Type = Seq<u8>

The view of [Combinator::Result].

fn wf(&self, v: Self::Type) -> bool

fn requires(&self) -> bool

impl View for Tail

open spec fn view(&self) -> Self::V

{ Tail }

type V = Tail

Auto Trait Implementations§

impl Freeze for Tail

impl RefUnwindSafe for Tail

impl Send for Tail

impl Sync for Tail

impl Unpin for Tail

impl UnwindSafe for Tail

Blanket Implementations§

impl<T> Any for T
where T: 'static + ?Sized,

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more

impl<T> Borrow<T> for T
where T: ?Sized,

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more

impl<T> BorrowMut<T> for T
where T: ?Sized,

fn borrow_mut(&mut self) -> &mut T

Mutably borrows from an owned value. Read more

impl<T> CloneToUninit for T
where T: Clone,

unsafe fn clone_to_uninit(&self, dest: *mut u8)

🔬This is a nightly-only experimental API. (clone_to_uninit)

Performs copy-assignment from self to dest. Read more

impl<T> From<T> for T
where T: View, <T as View>::V: SpecFrom<<T as View>::V>,

exec fn ex_from(t: T) -> res : T

impl<T> From<T> for T

fn from(t: T) -> T

Returns the argument unchanged.

impl<T, VERUS_SPEC__A> FromSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: From<T>,

fn obeys_from_spec() -> bool

fn from_spec(v: T) -> VERUS_SPEC__A

impl<T, U> Into<U> for T
where T: View, U: View + From<T>, <U as View>::V: SpecFrom<<T as View>::V>,

exec fn ex_into(self) -> U

impl<T, U> Into<U> for T
where U: From<T>,

fn into(self) -> U

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.

impl<T, VERUS_SPEC__A> IntoSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: Into<T>,

fn obeys_into_spec() -> bool

fn into_spec(self) -> T

impl<T, U> IntoSpecImpl<U> for T
where U: From<T>,

fn obeys_into_spec() -> bool

fn into_spec(self) -> U

impl<T> SpecFrom<T> for T

open spec fn spec_from(t: T) -> T

{ t }

impl<T, U> SpecInto<U> for T
where U: SpecFrom<T>,

open spec fn spec_into(self) -> U

{ U::spec_from(self) }

impl<T, U> SpecTryInto<U> for T
where U: SpecTryFrom<T>,

open spec fn spec_try_into(self) -> Result<U, <U as SpecTryFrom<T>>::Error>

{ U::spec_try_from(self) }

type Error = <U as SpecTryFrom<T>>::Error

The type returned in the event of a conversion error.

impl<T> ToOwned for T
where T: Clone,

type Owned = T

The resulting type after obtaining ownership.

fn to_owned(&self) -> T

Creates owned data from borrowed data, usually by cloning. Read more

fn clone_into(&self, target: &mut T)

Uses borrowed data to replace owned data, usually by cloning. Read more

impl<T, U> TryFrom<U> for T
where U: Into<T>,

type Error = Infallible

The type returned in the event of a conversion error.

fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>

Performs the conversion.

impl<T, VERUS_SPEC__A> TryFromSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: TryFrom<T>,

fn obeys_try_from_spec() -> bool

fn try_from_spec( v: T, ) -> Result<VERUS_SPEC__A, <VERUS_SPEC__A as TryFrom<T>>::Error>

impl<T, U> TryInto<U> for T
where T: View, U: View + TryFrom<T>, <U as View>::V: SpecTryFrom<<T as View>::V>,

exec fn ex_try_into(self) -> Result<U, <U as TryFrom<T>>::Error>

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.

impl<T, U> TryInto<U> for T
where U: TryFrom<T>,

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.

fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>

Performs the conversion.

impl<T, VERUS_SPEC__A> TryIntoSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: TryInto<T>,

fn obeys_try_into_spec() -> bool

fn try_into_spec(self) -> Result<T, <VERUS_SPEC__A as TryInto<T>>::Error>

impl<T, U> TryIntoSpecImpl<U> for T
where U: TryFrom<T>,

fn obeys_try_into_spec() -> bool

fn try_into_spec(self) -> Result<U, <U as TryFrom<T>>::Error>