Function nat_from_base128 

pub open spec fn nat_from_base128(bytes: Seq<u8>) -> nat

{
    if bytes.len() == 0 {
        0
    } else {
        nat_from_base128(bytes.drop_last()) * 128 + (bytes.last() % 128) as nat
    }
}

Unsigned big-endian base-128 decoding.