not_overlong_encoding

vstd::utf8

Function not_overlong_encoding 

Source 
pub open spec fn not_overlong_encoding(codepoint: u32, len: int) -> bool
Expand description
{
    &&& (len == 2 ==> 0x80 <= codepoint)
    &&& (len == 3 ==> 0x800 <= codepoint)
    &&& (len == 4 ==> 0x10000 <= codepoint <= 0x10ffff)

}

True when the given codepoint, when encoded in UTF-8 using len number of bytes, would not be an “overlong encoding”. An overlong encoding is one that uses more bytes than needed to encode the given value.