pub broadcast proof fn decode_utf8_encode_utf8(bytes: Seq<u8>)Expand description
requires
valid_utf8(bytes),#[trigger] encode_utf8(decode_utf8(bytes)) == bytes,Ensures that performing decode_utf8 followed by encode_utf8 results in the original byte sequence.