Function uint_to_base128_in_place 

pub exec fn uint_to_base128_in_place(v: UInt, obuf: &mut [u8])

requires

old(obuf)@.len() == nat_to_base128(v as nat).len(),

ensures

final(obuf)@ == nat_to_base128(v as nat),

Writes the minimal big-endian base-128 encoding of v into an exactly-sized slice.