Function partial_valid_utf8_extend

Source

pub broadcast proof fn partial_valid_utf8_extend(bytes: Seq<u8>, i: int)

Expand description

requires

#[trigger] partial_valid_utf8(bytes, i),

#[trigger] valid_first_scalar(bytes.subrange(i, bytes.len() as int)),

ensures

#[trigger]
partial_valid_utf8(
    bytes,
    i + length_of_first_scalar(bytes.subrange(i, bytes.len() as int)),
),

Ensures that if the prefix of a byte sequence is valid UTF-8, and remainder of the sequence begins with a valid UTF-8 encoding of a single scalar, then the prefix extended by that scalar encoding is also valid UTF-8.

partial_valid_utf8_extend

Function partial_valid_utf8_extend Copy item path

Function partial_valid_utf8_extend