pub broadcast proof fn is_char_boundary_iff_not_is_continuation_byte(bytes: Seq<u8>, index: int)Expand description
requires
valid_utf8(bytes),0 <= index < bytes.len(),#[trigger] is_char_boundary(bytes, index) <==> !(#[trigger]
is_continuation_byte(bytes[index])),Ensures that any byte in a valid UTF-8 byte sequence falls on a character boundary (i.e. the first byte in a codepoint’s encoding) if and only if it does not have the form of a UTF-8 continuation byte.