pub broadcast proof fn encode_utf8_valid_utf8(chars: Seq<char>)Expand description
ensures
valid_utf8(#[trigger] encode_utf8(chars)),Ensures the result of encode_utf8 always satisfies valid_utf8.
pub broadcast proof fn encode_utf8_valid_utf8(chars: Seq<char>)valid_utf8(#[trigger] encode_utf8(chars)),Ensures the result of encode_utf8 always satisfies valid_utf8.