UnsignedLEB128

vest_lib::regular::leb128

Struct UnsignedLEB128

pub struct UnsignedLEB128;

Expand description

Unsigned LEB128

Implementations§

impl UnsignedLEB128

pub open spec fn spec_serialize_helper(v: UInt) -> Seq<u8>

{
    let lo = take_low_7_bits!(v);
    let hi = v >> 7;
    if hi == 0 {
        seq![lo]
    } else {
        seq![set_high_8_bit!(lo)] + Self::spec_serialize_helper(hi)
    }
}

Helper function for spec_serialize

Trait Implementations§

impl<'x, I, O> Combinator<'x, I, O> for UnsignedLEB128
where I: VestPublicInput, O: VestPublicOutput<I>,

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

exec fn parse(&self, ss: I) -> res : PResult<Self::Type, ParseError>

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

type Type = u64

The result type of parsing

type SType = &'x u64

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 UnsignedLEB128

open spec fn is_prefix_secure() -> bool

{ true }

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

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

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

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

open spec fn is_productive(&self) -> bool

{ true }

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 UnsignedLEB128

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

{
    let v = take_low_7_bits!(s.first());
    if s.len() != 0 {
        if is_high_8_bit_set!(s.first()) {
            match self.spec_parse(s.drop_first()) {
                Some((n, v2)) => {
                    if n < usize::MAX
                        && 0 < v2 <= n_bit_max_unsigned!(8 * uint_size!() - 7)
                    {
                        Some((n + 1, v2 << 7 | v as Self::Type))
                    } else {
                        None
                    }
                }
                None => None,
            }
        } else {
            Some((1, v as Self::Type))
        }
    } else {
        None
    }
}

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

{ Self::spec_serialize_helper(v) }

type Type = u64

The view of [Combinator::Result].

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

fn requires(&self) -> bool

impl View for UnsignedLEB128

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

{ Self }

type V = UnsignedLEB128

Auto Trait Implementations§

impl Freeze for UnsignedLEB128

impl RefUnwindSafe for UnsignedLEB128

impl Send for UnsignedLEB128

impl Sync for UnsignedLEB128

impl Unpin for UnsignedLEB128

impl UnwindSafe for UnsignedLEB128

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>