Fail

vest_lib::regular::fail

Struct Fail

pub struct Fail(pub String);

Expand description

Combinator used for custom error message

Tuple Fields§

§0: String

Trait Implementations§

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

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

The result type of parsing

type SType = ()

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<T> DisjointFrom<T> for Fail
where T: SpecCombinator,

open spec fn disjoint_from(&self, c: &T) -> bool

{ true }

proof fn parse_disjoint_on(&self, c: &T, buf: Seq<u8>)

impl SecureSpecCombinator for Fail

open spec fn is_prefix_secure() -> bool

{ true }

open spec fn is_productive(&self) -> bool

{ false }

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

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

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

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

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 Fail

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

{ false }

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

{ None }

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

{ Seq::empty() }

type Type = ()

The view of [Combinator::Result].

fn requires(&self) -> bool

impl View for Fail

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

{ *self }

type V = Fail

Auto Trait Implementations§

impl Freeze for Fail

impl RefUnwindSafe for Fail

impl Send for Fail

impl Sync for Fail

impl Unpin for Fail

impl UnwindSafe for Fail

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