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