Function nat_to_base128 

pub open spec fn nat_to_base128(n: nat) -> Seq<u8>

{
    if n < 128 {
        seq![n as u8]
    } else {
        nat_to_base128((n / 128) as nat).push((n % 128) as u8)
    }
}

Unsigned big-endian base-128 encoding.