pub open spec fn partial_valid_utf8(bytes: Seq<u8>, i: int) -> bool
{ 0 <= i <= bytes.len() && valid_utf8(bytes[..i]) }
True when the first i bytes in the given sequence represent a valid UTF-8 encoding.
i