Struct Variable

pub struct Variable(pub usize);

Expand description

Combinator for parsing and serializing a fixed number of bytes (dynamically known).

Tuple Fields§

Implementations§

{ AndThen(self, next) }

o@ == self@.spec_and_then(next@),

Chains this combinator with another combinator.

Trait Implementations§

out == *self,

Performs copy-assignment from source. Read more

The result type of parsing

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.

{ true }

{ self.0 > 0 }

{ v.len() == self.0 }

{ if self.0 <= s.len() { Some((self.0 as int, s.take(self.0 as int))) } else { None } }

{ v }

The view of [Combinator::Result].

{ *self }

Auto Trait Implementations§

Blanket Implementations§

Gets the TypeId of self. Read more

Immutably borrows from an owned value. Read more

Mutably borrows from an owned value. Read more

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

Performs copy-assignment from self to dest. Read more

Returns the argument unchanged.

§

§

§

Calls U::from(self).

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

{ t }

{ U::spec_from(self) }

{ U::spec_try_from(self) }

The type returned in the event of a conversion error.

The resulting type after obtaining ownership.

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

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

The type returned in the event of a conversion error.

Performs the conversion.

§

§

§

The type returned in the event of a conversion error.

The type returned in the event of a conversion error.

Performs the conversion.

Struct Variable Copy item path

Tuple Fields§

Implementations§

impl Variable

pub open spec fn spec_and_then<Next: SpecCombinator>( self, next: Next, ) -> AndThen<Variable, Next>

pub exec fn and_then<'x, I, O, Next: Combinator<'x, I, O>>( self, next: Next, ) -> o : AndThen<Variable, Next>where I: VestPublicInput, O: VestPublicOutput<I>, Next::V: SecureSpecCombinator<Type = <Next::Type as View>::V>,

Trait Implementations§

impl Clone for Variable

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

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

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

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

type SType = &'x I

fn ex_requires(&self) -> bool

impl SecureSpecCombinator for Variable

open spec fn is_prefix_secure() -> bool

open spec fn is_productive(&self) -> bool

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 Variable

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

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

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

type Type = Seq<u8>

fn requires(&self) -> bool

impl View for Variable

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

type V = Variable

Auto Trait Implementations§

impl Freeze for Variable

impl RefUnwindSafe for Variable

impl Send for Variable

impl Sync for Variable

impl Unpin for Variable

impl UnwindSafe for Variable

Blanket Implementations§

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

fn type_id(&self) -> TypeId

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

fn borrow(&self) -> &T

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

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

impl<T> CloneToUninit for Twhere T: Clone,

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

impl<T> From<T> for Twhere 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

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

fn obeys_from_spec() -> bool

fn from_spec(v: T) -> VERUS_SPEC__A

impl<T, U> Into<U> for Twhere 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 Twhere U: From<T>,

fn into(self) -> U

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

fn obeys_into_spec() -> bool

fn into_spec(self) -> T

impl<T, U> IntoSpecImpl<U> for Twhere 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

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

open spec fn spec_into(self) -> U

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

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

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

impl<T> ToOwned for Twhere T: Clone,

Struct Variable

pub exec fn and_then<'x, I, O, Next: Combinator<'x, I, O>>( self, next: Next, ) -> o : AndThen<Variable, Next>
where I: VestPublicInput, O: VestPublicOutput<I>, Next::V: SecureSpecCombinator<Type = <Next::Type as View>::V>,

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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