pub broadcast proof fn decode_utf8_split(bytes: Seq<u8>, index: int)Expand description
requires
valid_utf8(bytes),is_char_boundary(bytes, index),decode_utf8(bytes) =~= decode_utf8(bytes[..index]) + decode_utf8(bytes[index..]),Ensures that a valid UTF-8 byte sequence can be decoded by separately decoding the two subsequences formed by splitting the original sequence at a character boundary.