partial_valid_utf8_extend_ascii_block

vstd::utf8

Function partial_valid_utf8_extend_ascii_block 

Source 
pub broadcast proof fn partial_valid_utf8_extend_ascii_block(
    bytes: Seq<u8>,
    start: int,
    end: int,
)
Expand description
requires
forall |i: int| {
    0 <= start <= i < end <= bytes.len() ==> #[trigger] is_leading_byte_width_1(bytes[i])
},
partial_valid_utf8(bytes, start),
0 <= start <= end <= bytes.len(),
ensures
partial_valid_utf8(bytes, end),

Ensures that if the prefix of a byte sequence is valid UTF-8, and remainder of the sequence begins with a subsequence of valid UTF-8 encodings for 1-byte scalars (i.e. ASCII characters), then the prefix extended by that subsequence is also valid UTF-8.