Function partial_valid_partial_invalid_utf8 

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

requires

0 <= i <= bytes.len(),

valid_utf8(bytes[..i]),

!valid_utf8(bytes[i..]),

ensures

!valid_utf8(bytes),

Ensures that a byte sequence is not a valid UTF-8 byte sequence when it has a suffix that is not a valid UTF-8 byte sequence.