pub broadcast proof fn is_ascii_chars_encode_utf8(chars: Seq<char>)Expand description
requires
#[trigger] is_ascii_chars(chars),chars.len() == encode_utf8(chars).len(),forall |i| 0 <= i < chars.len() ==> chars[i] as u8 == encode_utf8(chars)[i],Ensures that the UTF-8 encoding for an ASCII character sequence has the same length of the original sequence and corresponds byte-by-byte to the characters in the original sequence.