Function uint_from_base128 

pub exec fn uint_from_base128(bytes: &[u8]) -> result : UInt

requires

bytes.len() <= BASE128_MAX_BYTES,

ensures

result as nat == nat_from_base128(bytes.deep_view()),