pub broadcast proof fn valid_utf8_split(bytes: Seq<u8>, index: int)Expand description
requires
valid_utf8(bytes),is_char_boundary(bytes, index),valid_utf8(bytes.subrange(0, index)),valid_utf8(bytes.subrange(index, bytes.len() as int)),Ensures that the two subsequences formed by splitting a valid UTF-8 byte sequence at a character boundary are also valid UTF-8 byte sequences.