pub broadcast proof fn utf8_byte_ranges_bitwise(b: u8)Expand description
ensures
0x00 <= b <= 0x7f <==> b & 0x80 == 0,0xc0 <= b <= 0xdf <==> b & 0xe0 == 0xc0,0xe0 <= b <= 0xef <==> b & 0xf0 == 0xe0,0xf0 <= b <= 0xf7 <==> b & 0xf8 == 0xf0,0x80 <= b <= 0xbf <==> b & 0xc0 == 0x80,Formulates the byte ranges for each type of byte in UTF-8 (leading and continuation) in terms of bitwise operators instead of ranges.