Function base128_fmt 

pub open spec fn base128_fmt<const MINIMAL: bool>() -> Base128Fmt__<MINIMAL>

{
    Mapped {
        inner: Refined(
            Repeat(
                Refined(U8, |b: u8| b & CONTINUATION_MASK != 0),
                Refined(U8, |b: u8| b & CONTINUATION_MASK == 0),
            ),
            |pair: (Seq<u8>, u8)| {
                let (cont_bytes, term_byte) = pair;
                &&& cont_bytes.len() <= BASE128_MAX_BYTES - 1
                &&& MINIMAL
                    ==> (cont_bytes.len() > 0 ==> cont_bytes[0] & PAYLOAD_MASK != 0)

            },
        ),
        mapper: (
            |pair: (Seq<u8>, u8)| {
                let (cont_bytes, term_byte) = pair;
                let bytes = cont_bytes.push(term_byte);
                nat_from_base128(bytes) as UInt
            },
            |n: UInt| {
                let bytes = nat_to_base128(n as nat);
                let cont_bytes = bytes
                    .drop_last()
                    .map_values(|b: u8| b | CONTINUATION_MASK);
                let term_byte = bytes.last();
                (cont_bytes, term_byte)
            },
        ),
    }
}