is_char_boundary_iff_is_leading_byte

vstd::utf8

Function is_char_boundary_iff_is_leading_byte 

Source 
pub broadcast proof fn is_char_boundary_iff_is_leading_byte(bytes: Seq<u8>, index: int)
Expand description
requires
valid_utf8(bytes),
0 <= index < bytes.len(),
ensures
is_char_boundary(bytes, index)
    <==> (is_leading_byte_width_1(bytes[index]) || is_leading_byte_width_2(bytes[index])
        || is_leading_byte_width_3(bytes[index])
        || is_leading_byte_width_4(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 has the form of a UTF-8 leading byte.