Function varint_fmt 

pub open spec fn varint_fmt<const MINIMAL: bool>() -> VarIntFmt<MINIMAL>

{
    Mapped {
        inner: Bind(
            U8,
            |b1: u8| match b1 {
                b if b < VARINT_TAG_U16 => L(Empty),
                VARINT_TAG_U16 => {
                    R(L(Refined(U16Le, |v| MINIMAL ==> VARINT_TAG_U16 <= v)))
                }
                VARINT_TAG_U32 => R(R(L(Refined(U32Le, |v| MINIMAL ==> u16::MAX < v)))),
                VARINT_TAG_U64 => {
                    R(R(R(L(Refined(U64Le, |v| MINIMAL ==> u32::MAX < v)))))
                }
                _ => R(R(R(R(Void("Impossible"))))),
            },
        ),
        mapper: (
            |parsed: (u8, Sum<(), Sum<u16, Sum<u32, Sum<u64, Never>>>>)| match parsed {
                (b, L(_)) => b as u64,
                (VARINT_TAG_U16, R(L(v))) => v as u64,
                (VARINT_TAG_U32, R(R(L(v)))) => v as u64,
                (VARINT_TAG_U64, R(R(R(L(v))))) => v,
                _ => arbitrary(),
            },
            |v: u64| {
                match v {
                    v if v < VARINT_TAG_U16 as u64 => (v as u8, L(())),
                    v if v <= u16::MAX as u64 => (VARINT_TAG_U16, R(L(v as u16))),
                    v if v <= u32::MAX as u64 => (VARINT_TAG_U32, R(R(L(v as u32)))),
                    _ => (VARINT_TAG_U64, R(R(R(L(v))))),
                }
            },
        ),
    }
}