Struct ULeb128 

pub struct ULeb128<const MINIMAL: bool, const N: usize>;

Trait Implementations

impl<const MINIMAL: bool, const N: usize> Consistency for ULeb128<MINIMAL, N>

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

{ uleb128_fmt::<MINIMAL, N>().consistent(v) }

type Val = nat

The type of values whose consistency is being checked.

impl<const MINIMAL: bool, const N: usize> EquivSerializers for ULeb128<MINIMAL, N>

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

fn equiv_inv(&self) -> bool

impl<const MINIMAL: bool, const N: usize> EquivSerializersGeneral for ULeb128<MINIMAL, N>

proof fn lemma_serialize_equiv(&self, v: Self::SVal, obuf: Seq<u8>)

fn equiv_general_inv(&self) -> bool

impl<const MINIMAL: bool, const N: usize> GoodSerializer for ULeb128<MINIMAL, N>

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

fn serialize_inv(&self) -> bool

impl<const MINIMAL: bool, const N: usize> NoLookAhead for ULeb128<MINIMAL, N>

proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>)

fn no_lookahead_inv(&self) -> bool

fn corollary_non_extensible(&self, i1: Seq<u8>, i2: Seq<u8>)

impl<const N: usize> NonMalleable for ULeb128<true, N>

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

fn nonmal_inv(&self) -> bool

impl<const MINIMAL: bool, const N: usize> NonTailFmt for ULeb128<MINIMAL, N>

proof fn lemma_serialize_dps_prepend(&self, v: Self::SValue, obuf: Seq<u8>)

proof fn lemma_serialize_dps_len(&self, v: Self::SValue, obuf: Seq<u8>)

fn serialize_dps_inv(&self) -> bool

impl<const MINIMAL: bool, const N: usize> Productive for ULeb128<MINIMAL, N>

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

fn productive_inv(&self) -> bool

impl<const MINIMAL: bool, const N: usize> SPRoundTripDps for ULeb128<MINIMAL, N>

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

fn unambiguous(&self) -> bool

impl<const MINIMAL: bool, const N: usize> SafeParser for ULeb128<MINIMAL, N>

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

fn safe_inv(&self) -> bool

impl<const N: usize> SoundParser for ULeb128<true, N>

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<const MINIMAL: bool, const N: usize> SpecByteLen for ULeb128<MINIMAL, N>

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

{ uleb128_fmt::<MINIMAL, N>().byte_len(v) }

type T = nat

The type of values whose byte length is being computed.

impl<const MINIMAL: bool, const N: usize> SpecParser for ULeb128<MINIMAL, N>

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

{ uleb128_fmt::<MINIMAL, N>().spec_parse(ibuf) }

type PVal = nat

The type of parsed values.

impl<const MINIMAL: bool, const N: usize> SpecSerializer for ULeb128<MINIMAL, N>

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

{ uleb128_fmt::<MINIMAL, N>().spec_serialize(v) }

type SVal = nat

The type of values to be serialized.

impl<const MINIMAL: bool, const N: usize> SpecSerializerDps for ULeb128<MINIMAL, N>

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

{ uleb128_fmt::<MINIMAL, N>().spec_serialize_dps(v, obuf) }

type SValue = nat

The type of values to be serialized.