valid_first_scalar

vstd::utf8

Function valid_first_scalar 

Source 
pub open spec fn valid_first_scalar(bytes: Seq<u8>) -> bool
Expand description
{
    &&& valid_leading_and_continuation_bytes_first_codepoint(bytes)
    &&& not_overlong_encoding(
        decode_first_codepoint(bytes),
        length_of_first_codepoint(bytes),
    )
    &&& not_surrogate(decode_first_codepoint(bytes))

}

True when the given byte sequence begins with a well-formed UTF-8 encoding of a single scalar. To be a well-formed encoding, the bytes must: follow the expected bit pattern for leading and continuation bytes for a single scalar encoding, not be an “overlong encoding”, and not fall in the surrogate range.