Struct ULeb128RecBody 

pub struct ULeb128RecBody<const MINIMAL: bool>;

Trait Implementations

impl<const MINIMAL: bool> EquivSerializersGeneralRecBody for ULeb128RecBody<MINIMAL>

proof fn lemma_s_body_equiv_general_inv_preservation( &self, _param: (), rec: ParamRecSpecs<Self::Param, Self::T>, )

impl<const MINIMAL: bool> GoodSerializerRecBody for ULeb128RecBody<MINIMAL>

proof fn lemma_s_body_serialize_inv_preservation( &self, _param: (), rec: ParamRecSpecs<Self::Param, Self::T>, )

impl<const MINIMAL: bool> NoLookAheadRecBody for ULeb128RecBody<MINIMAL>

proof fn lemma_body_no_lookahead_inv_preservation( &self, _param: (), rec: ParamRecSpecs<Self::Param, Self::T>, )

impl NonMalleableRecBody for ULeb128RecBody<true>

proof fn lemma_body_nonmal_inv_preservation( &self, _param: (), rec: ParamRecSpecs<Self::Param, Self::T>, )

impl<const MINIMAL: bool> NonTailFmtRecBody for ULeb128RecBody<MINIMAL>

proof fn lemma_s_body_dps_serialize_dps_inv_preservation( &self, _param: (), rec: ParamRecSpecs<Self::Param, Self::T>, )

impl<const MINIMAL: bool> ProductiveRecBody for ULeb128RecBody<MINIMAL>

proof fn lemma_body_productive_inv_preservation( &self, param: Self::Param, rec: ParamRecSpecs<Self::Param, Self::T>, )

impl<const MINIMAL: bool> SPRoundTripDpsRecBody for ULeb128RecBody<MINIMAL>

proof fn lemma_body_sp_roundtrip_dps_inv_preservation( &self, _param: (), rec: ParamRecSpecs<Self::Param, Self::T>, )

impl<const MINIMAL: bool> SafeParserRecBody for ULeb128RecBody<MINIMAL>

proof fn lemma_body_safe_inv_preservation( &self, _param: (), rec: ParamRecSpecs<Self::Param, Self::T>, )

impl SoundParserRecBody for ULeb128RecBody<true>

proof fn lemma_body_sound_inv_preservation( &self, _param: (), rec: ParamRecSpecs<Self::Param, Self::T>, )

impl<const MINIMAL: bool> SpecRecBody for ULeb128RecBody<MINIMAL>

open spec fn spec_body( &self, _param: (), rec: ParamRecSpecs<Self::Param, Self::T>, ) -> Self::Body

{
    Alt(
        terminal_byte_nat(),
        Mapped {
            inner: Pair(
                continuation_byte(),
                Refined(rec(()), |v: nat| MINIMAL ==> v > 0),
            ),
            mapper: (
                |pair: (u8, nat)| 128 * pair.1 + pair.0 as nat,
                |o: nat| ((o % 128) as u8, o / 128),
            ),
        },
    )
}

𝚞𝑁 ::= 𝑛:𝚋𝚢𝚝𝚎 ⇒ 𝑛 if 𝑛 < 2^7

| 𝑛:𝚋𝚢𝚝𝚎 𝑚:𝚞(𝑁−7) ⇒ 2^7 * 𝑚 + (𝑛 − 2^7) if 𝑛 >= 2^7

type Param = ()

type T = nat

type Body = Alt<Mapped<Refined<U8, FnSpec<(u8,), bool>>, TermByteFromToNat>, Mapped<Pair<Mapped<Refined<U8, FnSpec<(u8,), bool>>, LowBitsMask>, Refined<(FnSpec<(nat,), bool>, FnSpec<(nat,), nat>, FnSpec<(Seq<u8>,), Option<(int, nat)>>, FnSpec<(nat,), Seq<u8>>, FnSpec<(nat, Seq<u8>), Seq<u8>>), FnSpec<(nat,), bool>>>, (FnSpec<((u8, nat),), nat>, FnSpec<(nat,), (u8, nat)>)>>