decode_utf8_split

vstd::utf8

Function decode_utf8_split 

Source 
pub broadcast proof fn decode_utf8_split(bytes: Seq<u8>, index: int)
Expand description
requires
valid_utf8(bytes),
is_char_boundary(bytes, index),
ensures
decode_utf8(bytes)
    =~= decode_utf8(bytes.subrange(0, index))
        + decode_utf8(bytes.subrange(index, bytes.len() as int)),

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.